proposition: Corollary iipc2_is_safe_environment {Gamma x} : iipc2 Gamma (poly_var x) -> Forall (is_safe_poly_type 0) Gamma -> exists ss ts, In (safe_poly_type (length ts) ss x) Gamma /\ Forall (iipc2 Gamma) (map (subst_poly_type (fold_right scons poly_var (rev ts))) ss).
proof: Proof. move=> [P] /typing_normal_form [{}P] [/typing_is_safe_environment H] /H {}H /H. move=> [ss] [?] [ts] [?] [_] [/nth_error_In ?] /Forall2_typing_Forall_iipc2 ?. by exists ss, ts. Qed.
imports: PeanoNat List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts term_facts typing_facts iipc2_facts sn_facts) Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun