proposition: Lemma step'E M N : step' M N -> match M with | var _ => False | app M1 M2 => normal_form M2 /\ match M1 with | var _ => False | app _ _ => exists M', step' M1 M' | lam M3 => normal_form M3 /\ N = (subst (scons M2 var) M3) end | lam _ => False end.
proof: Proof. case; [tauto|case]. - move=> > _ H. inversion H. - move=> *. split; [|eexists]; eassumption. - move=> > _ H. inversion H. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect