-
-(*
-lemma SH_Lambda: ∀N.SH N → ∀M.SH M → SN (Lambda N M).
-#N #snN (elim snN) #P #snP #HindP #M #snM (elim snM)
-#Q #snQ #HindQ % #a #redH (cases (red_lambda … redH))
- [*
- [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) /2/
- % /2/
- |* #S * #eqa #redQS >eqa @(HindQ S) /2/
- ]
- |* #S * #eqQ #eqa >eqa @SN_d @(HindQ S) /3/
- ]
-qed. *)