proposition: Lemma var_bound_spec M : allfv (fun x => x < var_bound M) M.
proof: Proof. elim: M=> /=. - lia. - move=> ? IH1 ? IH2. split. + apply: allfv_impl IH1. lia. + apply: allfv_impl IH2. lia. - move=> ?. by apply: allfv_impl=> - [|?] /=; [|lia]. Qed.
imports: Undecidability.IntersectionTypes(CD Util.CD_facts) Undecidability.LambdaCalculus.Util.term_facts List PeanoNat Lia ssreflect