proposition: Lemma snE M : sn M -> match M with | var x => True | app M N => sn M /\ sn N | lam M => sn M end.
proof: Proof. elim. case. - done. - move=> M1 M2 IH1 IH2. split. + by constructor=> ? /(stepAppL _ _ M2) /IH2 []. + by constructor=> ? /(stepAppR M1) /IH2 []. - move=> M1 IH1 IH2. by constructor=> ? /stepLam /IH2. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect