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