proposition: Lemma typing_safe_poly_typeE {Gamma P n ss x As y} : typing Gamma P (many_poly_abs n (many_poly_arr ss (poly_var (n+x)))) -> typing Gamma (many_argument_app P As) (poly_var y) -> exists (ts : list poly_type) (Qs : list term), x = y /\ As = (map argument_poly_type ts) ++ (map argument_term Qs) /\ n = length ts /\ length ss = length Qs.
proof: Proof. elim: n P ss x As. - move=> P ss x As /=. elim: ss P As. + move=> P [| [?|?] ?]. * move=> /typing_functional H /H [] ->. by exists [], []. * move=> /= + /typing_many_argument_subterm [?] /typingE [?]. by move=> /typing_functional H [/H]. * move=> /= + /typing_many_argument_subterm [?] /typingE [?]. by move=> /typing_functional H [_ /H]. + move=> s ss IH P [| [Q|?] ?] /=. * by move=> /typing_functional H /H. * move=> + /[dup] [/IH {}IH]. move=> + /typing_many_argument_subterm [?] /[dup] [/typingE [?]]. move=> /typing_functional H [/H{H} [<-]] <- ? /IH. move=> [[| ? ?]] [Qs] [<-] [->] [?] ->; last done. by exists [], (Q :: Qs). * move=> + /typing_many_argument_subterm [?] /typingE [?]. by move=> /typing_functional H [_ /H]. - move=> n IH P ss x [|A As] /=. + by move=> /typing_functional H /H. + move: A => [? | s]. * move=> + /typing_many_argument_subterm [?] /typingE [?]. by move=> /typing_functional H [/H]. * move=> /typing_ty_app => /(_ s). rewrite subst_poly_type_many_poly_abs subst_poly_type_many_poly_arr /=. have ->: S (n + x) = n + S x by lia. rewrite iter_up_poly_type_poly_type. move=> /IH {}IH /IH. move=> [ts] [Qs] [<-] [->] [->]. rewrite map_length. move=> ->. by exists (s :: ts), Qs. 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