proposition: Lemma normal_formE M : normal_form M -> match M with | var _ => True | app M N => match M with | var _ => normal_form N | app _ _ => normal_form M /\ normal_form N | lam _ => False end | lam M => normal_form M end.
proof: Proof. by case. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect