proposition: Lemma head_exp_sn M N : head_exp sn M N -> sn M -> sn N.
proof: Proof. move=> /head_exp'I [L] H1 /Acc_clos_trans H2. elim: H2 N L H1=> {}M IH1M IH2M N L H'. have H : sn L by elim H'. elim: H M IH1M IH2M N H' => {}L IH1L IH2L M IH1M IH2M N. move=> /head_exp'_step HMN. constructor=> N' /HMN [|[|]]. - move=> <-. apply: Acc_clos_trans'. by constructor. - by move=> [M'] [] /clos_trans_flip /IH2M /[apply]. - move=> [L'] [/IH2L] {}IH2L [M'] [/clos_refl_trans_flip ? /IH2L]. apply. + move=> ??. apply: IH1M. apply: clos_rt_t'; eassumption. + move=> ????. apply: IH2M. apply: clos_rt_t'; eassumption. 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