proposition: Lemma allfv_poly_type_many_poly_absI {P n t} : allfv_poly_type (Nat.iter n (scons True) P) t -> allfv_poly_type P (many_poly_abs n t).
proof: Proof. elim: n P; first done. move=> n IH P. by rewrite -iter_last => /IH. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun