proposition: Lemma allfv_poly_type_many_poly_arrI {P ss x} : Forall (allfv_poly_type P) ss -> P x -> allfv_poly_type P (many_poly_arr ss (poly_var x)).
proof: Proof. elim: ss; first done. move=> > IH /Forall_cons_iff [? /IH {}IH] /IH ?. by constructor. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun