なんか、Leanって結局は証明を書くことが主目的で、その主張に矛盾がないかを一応自動で検証してくれる環境であって、SMTソルバーみたいに推論してくれる環境ではないんだね・・・＞＜
目的外に使おうとすると、全部言われないとわからない呑み込みが悪い人的な環境＞＜；