proposition: Lemma head_exp'_step M N N' L : head_exp' sn M N L -> step N N' -> M = N' \/ (exists M', clos_trans _ step M M' /\ head_exp' sn M' N' L) \/ (exists L', step L L' /\ (exists M', clos_refl_trans _ step M M' /\ head_exp' sn M' N' L')).
proof: Proof. move=> + H. elim: H M L. - move=> > /head_exp'E []. + move=> [?] [[->]] [->] [->] ?. by left. + by move=> [?] [?] [/head_exp'E]. - move=> > H IH ? ? /head_exp'E []. + move=> [?] [?] [?] [??]. subst. right. left. move: H => /stepE [?] [??]. subst. eexists. split; [|by constructor]. apply: t_step. by apply: subst_step. + move=> [?] [?] [+?]. move=> /IH [|[|]]. * move=> ?. subst. by left. * move=> [?] [??]. subst. right. left. eexists. split; [|constructor; eassumption]. by apply: t_stepsAppL. * move=> [?] [?] [?] [??]. subst. right. right. eexists. split; [eassumption|]. eexists. split; [|constructor; eassumption]. by apply: rt_stepsAppL. - move=> > ? _ ?? /head_exp'E [|]. + move=> [?] [?] [?] [??]. subst. right. right. eexists. split; [eassumption|]. eexists. split; [|constructor; apply: Acc_inv; eassumption]. apply: subst_steps=> - [|?] /=; by eauto using clos_refl_trans. + move=> [?] [?] [??]. subst. right. left. eexists. split; [|constructor; [|apply: Acc_inv]; eassumption]. apply: t_step. by apply: stepAppR. - by move=> > ? _ ?? /head_exp'E. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations List Wellfounded.Transitive_Closure ssreflect