proposition: Lemma typing_many_app_arguments {Gamma P Qs t ss t'} : length Qs = length ss -> typing Gamma (many_app P Qs) t -> typing Gamma P (many_poly_arr ss t') -> Forall2 (typing Gamma) Qs ss.
proof: Proof. elim: Qs P t ss t'. - move=> ? ? [|] *; [by constructor | done]. - move=> Q Qs IH P ? [|? ?] ?; first done. move=> [/IH {}IH] /= /[dup] [/IH {}IH]. rewrite -many_argument_app_map_argument_term. move=> /typing_many_argument_subterm [?]. move=> /[dup] [/typingE [?] [+ ?]]. move=> /typing_functional H + /H{H} [? ?]. subst. move=> /IH ?. by constructor. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts term_facts) ssreflect ssrbool ssrfun