proposition: Lemma allfv_ren (P : nat -> Prop) xi t : allfv (funcomp P xi) t -> allfv P (ren xi t).
proof: Proof. elim: t P xi. - done. - move=> ? IH1 ? IH2 > /= [??]. by auto. - move=> ? IH > /= H. apply: IH. by apply: allfv_impl H => - [|?]. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect