proposition: Lemma typing_is_safe_environment {Gamma P x} : normal_form P -> typing Gamma P (poly_var x) -> Forall (is_safe_poly_type 0) Gamma -> exists ss y ts Qs, P = many_app (many_ty_app (var y) ts) Qs /\ nth_error Gamma y = Some (safe_poly_type (length ts) ss x) /\ Forall2 (typing Gamma) Qs (map (subst_poly_type (fold_right scons poly_var (rev ts))) ss).
proof: Proof. case; [ | by move=> > _ /typingE [?] [] | by move=> > _ /typingE [?] []]. move=> {}P /many_argument_appI [y] [As] [-> _]. move=> /[dup] [/typing_many_argument_subterm [?]]. move=> /[dup] [/typingE]. move=> + + + /Forall_forall H => /nth_error_In /H{H} /is_safe_poly_typeE. move=> [n] [ss] [z] -> Hy HyAs. exists ss, y. move: (Hy) (HyAs) => /typing_safe_poly_typeE H /H{H}. move=> [ts] [Qs] [?] [?] [? ?]. exists ts, Qs. subst x As. subst n. constructor; [|constructor]. - by rewrite many_argument_app_app many_argument_app_map_argument_poly_type many_argument_app_map_argument_term. - by move: Hy => /typingE. - move: Hy => /typing_many_ty_appI => /(_ ts ltac:(lia)). move: HyAs. rewrite many_argument_app_app many_argument_app_map_argument_poly_type. move: (many_ty_app (var y) _) => {}P. rewrite subst_poly_type_many_poly_arr many_argument_app_map_argument_term. move=> /typing_many_app_arguments H /H. apply. by rewrite map_length. 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