proposition: Lemma iipc2_Ut_unique {xs tSs tPs t} : iipc2 (Gamma0 ++ map Ut (map (fun x : nat => poly_var (x + zt)) xs) ++ map St tSs ++ map Pt tPs) (Ut t) -> exists n, encodes_nat t n.
proof: Proof. move=> /generalize_Gamma0 /generalize_GammaS /generalize_GammaP. move=> /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_is_safe_environment. apply: unnest. { do 3 (constructor; first by move=> /=; lia). apply: Forall_appI; first by apply: is_safe_environment_Ut. by do 2 (constructor; first by move=> /=; lia). } rewrite [[poly_var tt]]lock [[poly_var st]]lock [[poly_var pt]]lock. move=> [ss'] [ts'] [+ Hss] => /=. rewrite -lock /= in_app_iff in_map_iff /=. do 3 (case; first by move=> /last_poly_var_safe_poly_type). case; first last. { unlock. do 2 (case; first by move=> /last_poly_var_safe_poly_type). done. } move=> [tx]. rewrite in_map_iff. move=> [Hx] [x] [?] Hxxs. subst tx. exists x. move: Hx Hss => /(congr1 parameters_poly_arr). rewrite parameters_poly_arr_safe_poly_type /=. case: ts'; last done. move=> /= <-. rewrite ?app_comm_cons. move=> /Forall_cons_iff [+ /Forall_cons_iff [+ _]]. rewrite ?subst_poly_type_poly_var. unlock. move=> /generalize_GammaU H1 /generalize_GammaU H2. constructor. - move: H1 => /iipc2_poly_arrE /iipc2_is_safe_environment. clear. apply: unnest. { by do ? (constructor; first by move=> /=; lia). } move=> [ss] [ts] /= []. do 2 (case; first by move=> /last_poly_var_safe_poly_type). case; first last. { do 4 (case; first by move=> /last_poly_var_safe_poly_type). done. } move=> /(congr1 parameters_poly_arr). rewrite parameters_poly_arr_safe_poly_type /=. case: ts; last done. move=> /= <-. move=> /Forall_inv [?] /typing_abs /iipc2I. rewrite subst_poly_type_poly_var. apply: iipc2_generalization. by do 6 (constructor; first by (apply: last_poly_var_typingI; firstorder done)). - have ? : x + zt <> b2t by (rewrite /dt /zt /zt' /b2t; lia). move: H2 => /iipc2_poly_arrE /iipc2_is_safe_environment. apply: unnest. { by do ? (constructor; first by move=> /=; lia). } move=> [ss] [ts] /= []. case; first by (move=> /last_poly_var_safe_poly_type; case). case; first last. { do 5 (case; first by move=> /last_poly_var_safe_poly_type). done. } move=> /(congr1 parameters_poly_arr). rewrite parameters_poly_arr_safe_poly_type /=. case: ts; last done. move=> /= <-. move=> /Forall_inv [?] /typing_abs /iipc2I. clear. rewrite subst_poly_type_poly_var. move=> /iipc2_generalization => /(_ GammaC). apply: unnest. { by do 6 (constructor; first by (apply: last_poly_var_typingI; firstorder done)). } move=> [?] /(typing_app _) H. by have [? /H /iipc2I] := to_d_typingI (poly_var (x + zt)) t GammaC. 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