proposition: Lemma allfv_impl (P Q : nat -> Prop) t : (forall x, P x -> Q x) -> allfv P t -> allfv Q t.
proof: Proof. elim: t P Q => /=. - move=> >. by apply. - move=> ? IH1 ? IH2 > /[dup] /IH1 {}IH1 /IH2 {}IH2. tauto. - move=> > IH > H /=. apply: IH. by case. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect