proposition: Lemma Forall2_typing_Forall_iipc2 {Gamma Ps ts} : Forall2 (typing Gamma) Ps ts -> Forall (iipc2 Gamma) ts.
proof: Proof. elim; [by constructor | by move=> > /iipc2I; constructor]. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts typing_facts) ssreflect ssrbool ssrfun