proposition: Lemma poly_var_boundP t : allfv_poly_type (gt (poly_var_bound t)) t.
proof: Proof. elim: t. - move=> /=. by lia. - move=> ? IH1 ? IH2 /=. by constructor; [move: IH1 | move: IH2]; apply: allfv_poly_type_impl; lia. - move=> ? /=. apply: allfv_poly_type_impl. case; [done | by move=> /=; lia]. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun