proposition: Lemma colon_redex s t u : closed (lam s) -> closed (lam t) -> clos_trans step (colon (app (lam s) (lam t)) u) (colon (subst (scons (lam t) var) s) u).
proof: Proof. move=> /= Hs Ht. apply: t_trans. { apply: t_step. by apply: wCBN_stepSubst. } rewrite /=. apply: t_trans. { apply: t_step. apply: wCBN_stepApp. by apply: wCBN_stepSubst. } have /(steps_to_colon _ u) : closed (subst (scons (lam t) var) s). { move: Hs Ht => /closed_dcl /boundE ? /closed_dcl ?. apply /closed_dcl. apply: bound_subst; first by eassumption. move=> [|n]; [done|lia]. } rewrite !simpl_term /= cbv_cbn_subst. { by case. } congr clos_trans. congr app. 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)