proposition: Lemma ren_ren_term xi1 xi2 t : ren xi2 (ren xi1 t) = ren (funcomp xi2 xi1) t.
proof: Proof. elim: t xi1 xi2 => /=. - done. - move=> ? IH1 ? IH2 ??. by rewrite IH1 IH2. - move=> ? IH ??. rewrite IH. congr lam. apply: ext_ren_term. by case. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect