proposition: Lemma iipc2_poly_arr_comp {Gamma s r t} : iipc2 Gamma (poly_arr s r) -> iipc2 Gamma (poly_arr r t) -> iipc2 Gamma (poly_arr s t).
proof: Proof. move=> [?] /(@typing_ren_term' S) HP1 [?] /(@typing_ren_term' S) HP2. eexists. apply: typing_abs. apply: typing_app; first by apply: HP2. apply: typing_app; first by apply: HP1. by apply: (typing_var (x := 0)). Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts typing_facts) ssreflect ssrbool ssrfun