proposition: Lemma allfv_poly_type_TrueI {p: nat -> Prop} {t} : (forall x, p x) -> allfv_poly_type p t.
proof: Proof. move=> Hp. elim: t; [done | done |]. move=> /= ?. apply: allfv_poly_type_impl. case; first done. move=> *. by apply: Hp. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun