fact: Fixpoint allfv (P : nat -> Prop) t := match t with | var x => P x | app s t => allfv P s /\ allfv P t | lam t => allfv (scons True P) t end.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect