proposition: Lemma pure_var_boundP M : allfv_pure_term (gt (pure_var_bound M)) M.
proof: Proof. elim: M. - move=> /=. by lia. - move=> ? IH1 ? IH2 /=. constructor; [move: IH1 | move: IH2]; apply: allfv_pure_term_impl; by lia. - move=> ? /=. apply: allfv_pure_term_impl. case; first done. move=> /=. by lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts Undecidability.SystemF.Util.poly_type_facts ssreflect ssrbool ssrfun