proposition: Lemma flatten_cons u sigma s : subst (fun n : nat => ren (fun _ => 0) (scons u sigma n)) s = subst (scons (ren (fun _ => 0) u) var) (subst (scons (var 0) (funcomp (ren S) (funcomp (ren (fun _ => 0)) sigma))) s).
proof: Proof. rewrite /= !simpl_term. apply: ext_subst_term. move=> [|n] /=; first done. by rewrite !simpl_term ren_as_subst_term. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.term_facts) Undecidability.L.Util.L_facts List Lia Relations ssreflect