proposition: Lemma ext_ren_term xi1 xi2 t : (forall n, xi1 n = xi2 n) -> ren xi1 t = ren xi2 t.
proof: Proof. elim: t xi1 xi2. - move=> > /= ?. by congr var. - move=> ? IH1 ? IH2 ?? Hxi /=. congr app; [by apply: IH1 | by apply: IH2]. - move=> ? IH > Hxi /=. congr lam. apply: IH. case; first done. move=> ?. by congr S. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect