proposition: Lemma ext_allfv_ren_term xi1 xi2 t : allfv (fun x=> xi1 x = xi2 x) t -> ren xi1 t = ren xi2 t.
proof: Proof. move=> H. rewrite !ren_as_subst_term. apply: ext_allfv_subst_term. by apply: allfv_impl H => ? /= ->. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect