View Lemma．むずかしい….
まず，普通はあまり使わない向きかもしれないが，
bv1 /\ bv2 -> G
に対して
move/andP
を実行すると，
bv1 && bv2 -> G
になるメカニズムは，だいたい以下のようになっていると思われる．
andP の型は，reflect なので
(andP b1 b2 : reflect (b1 /\ b2) (b1 && b2))，
view hint に登録されている以下の6つのうちのどれかが使われて，
andP と top: bv1 /\ bv2が引数に渡される．
第1,2引数の P と b は，andP と top を渡したときにちゃんと型がつく
ように埋められるらしい．(reference manual Section 9.6)
Variables (P:Prop) (b c:bool). Lemma elimTF : reflect P b -> b = c -> if c then P else ~ P. Lemma elimNTF : reflect P b -> ~~ b = c -> if c then ~ P else P. Lemma elimTFn : reflect P (~~ b) -> b = c -> if c then ~ P else P. Lemma introT : reflect P b -> P -> b. Lemma introTn : reflect P (~~ b) -> ~ P -> b. Lemma introN : reflect P b -> ~ P -> ~~ b.
今回の場合，これでマッチするのは introT なのでこれが使われて，正確には
generalize (introT andP top)が実行されて，
bv1 && bv2 -> G になる，ということのようである．
reference manual には，この項の top の入り方が書かれてないのでイマイチよくわからないが．
さて，では，もっと普通に使う bv1 && bv2 -> G を bv1 /\ bv2 -> G
に直すのはどうなっているか．この場合，intro した時点で，導入される context は，
top : bv1 && bv2 に見えている．これだと
view_lemma andP top がどこともマッチしないように見えるが，
view lemma の2番目の引数の型のソートは Prop なので，coercion が効いて，
is_true (bv1 && bv2) 型 すなわち (bv1 && bv2) = true 型
と考えることもできる．こう考えると， b = bv1 && bv2, c = true
とマッチすることができて， elimTF andP top が
if true then bv1 /\ bv2 else ~ (bv1 /\ bv2) ，すなわち
bv1 /\ bv2 型になる．実際， generalize (elimTF andP top) と
してみると， bv1 /\ bv2 が挿入される．
DFSチュートリアルに出てきたものから，応用例を．
contextに正しくない boolean predicate，たとえば H: x + y < x があった
とする．ゴールGがなんであろうと無視して証明をしたい．
こういうときに，Hの否定の方の証明
(この場合， leq_addr y x : x <= x + y ）がすでにあれば，
case/idPn (leq_addr y x) とすればよい．
まず，idPn (b:bool) = reflect (~~b) (~~b) であるから， P が
~~ b で，elimTFn にマッチすることになる，move/idPn であれば，
~ (~~ b) -> G となるところであるが，case/idPn なら，ここで
さらに場合分けが行われる．別記事に書いたように，not の場合分けを行うと
ゴールが ~~ b となる．今の場合だと ~ (x <= x + y) なので，
たとえば by rewrite -leqNgt. で証明が終わる．ここで，
leqNgt a b = (a <= b) = ~~ (a < b) ．