proposition: Lemma steps_to_colon s u : closed s -> clos_trans step (app (cbv_cbn s) u) (colon s u).
proof: Proof. elim: s u. - by move=> > /not_closed_var. - move=> s IH1 t IH2 u /= /closed_app [/[dup] Hs /IH1 {}IH1 /IH2 {}IH2]. have {}IH1 := IH1 (lam (app (ren S (cbv_cbn t)) (lam (app (app (var 1) (var 0)) (ren S (ren S u)))))). have {}IH2 := IH2 (lam (app (app (ren S (Psi s)) (var 0)) (ren S u))). move: (s) Hs IH1 IH2 => []. + by move=> > /not_closed_var. + move=> s1 s2 _. move: (app s1 s2) => s' IH1 IH2. apply: t_trans. { apply: t_step. by apply: wCBN_stepSubst. } move: IH1. by rewrite /= !simpl_term !ren_as_subst_term. + move=> s' _ IH1 IH2. apply: t_trans. { apply: t_step. by apply: wCBN_stepSubst. } move: IH1 => /t_trans'. apply. { rewrite /= !simpl_term !ren_as_subst_term. congr app. congr lam. congr app. congr lam. apply: ext_subst_term. by case. } apply: t_trans. { apply: t_step. by apply: wCBN_stepSubst. } move: IH2. by rewrite /= !simpl_term !ren_as_subst_term. - move=> s IH u ?. apply: t_step. rewrite /=. apply: stepLam'. rewrite /= !simpl_term /=. congr app. congr lam. rewrite -[LHS]subst_var_term. apply: ext_subst_term. by case. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)