proposition: Lemma iipc2_to_dE {x y: nat} : dt < x -> dt < y -> iipc2 GammaC (poly_arr (to_d (poly_var x)) (to_d (poly_var y))) -> x = y.
proof: Proof. move=> Hx Hy /iipc2_poly_arrE /iipc2_poly_arrE /iipc2_is_safe_environment. move=> [:HGamma]. rewrite [GammaC]lock. apply: unnest. { abstract: HGamma. rewrite -lock. by do ? (constructor; first by move=> /=; lia). } move=> [ss] [ts] /= []. move=> [| [|]]. - move=> /last_poly_var_safe_poly_type []. by lia. - have -> : to_d (poly_var x) = safe_poly_type 0 [poly_var x] dt by done. move=> /safe_poly_type_eqE [+] [<- _]. case: ts; last done. move=> _ /Forall_inv /iipc2_is_safe_environment => /(_ HGamma). move=> [ss'] [ts'] /= []. move=> [| [|]]. + by move=> /last_poly_var_safe_poly_type [] <-. + move=> /safe_poly_type_eqE. by lia. + rewrite -lock /GammaC in_map_iff => [[?]] [+]. move=> /last_poly_var_safe_poly_type [->] /in_seq. move: Hx. rewrite /dt. by lia. - rewrite -lock /GammaC. move=> /in_map_iff [?] []. move=> /last_poly_var_safe_poly_type [->] /in_seq. move: Hx. rewrite /dt. by lia. 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