proposition: Lemma allfv_trivial (P : nat -> Prop) t : (forall x, P x) -> allfv P t.
proof: Proof. elim: t P=> /=; [by auto..|]. move=> ? IH *. by apply: IH => - [|?]. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect