proposition: Lemma encodes_nat_transport' {x s t1 t2 t3 n n1 n2 n3} : iipc2 ([poly_arr (to_d t3) (poly_var b3t); poly_arr (to_d t2) (poly_var b2t); poly_arr (to_d t1) (poly_var b1t); poly_var tt] ++ [poly_var ut] ++ [poly_var st] ++ [poly_var pt]) (poly_arr (to_d s) (poly_var x)) -> encodes_nat t1 n1 -> encodes_nat t2 n2 -> encodes_nat t3 n3 -> encodes_nat s n -> (x = b1t -> n = n1) /\ (x = b2t -> n = n2) /\ (x = b3t -> n = n3).
proof: Proof. have : (x <> b1t /\ x <> b2t /\ x <> b3t) \/ (x = b1t) \/ (x = b2t) \/ (x = b3t) by lia. case; first by lia. move=> Hx. move=> /iipc2_poly_arrE /iipc2_is_safe_environment. apply: unnest. { by do ? (constructor; first by move=> /=; lia). } move=> [ss] [ts] [+ Hss] => /=. case; first by move=> /last_poly_var_safe_poly_type [] ?; subst x. case. { move=> /[dup] [/(congr1 parameters_poly_arr) + /last_poly_var_safe_poly_type [{}Hx]]. rewrite parameters_poly_arr_safe_poly_type /=. case: ts Hss; last done. move=> /= + ?. subst x ss. move=> /Forall_inv. rewrite subst_poly_type_poly_var. by move=> /generalize_GammaC /encodes_nat_transport H _ _ /H {}H /H{H} ->. } case. { move=> /[dup] [/(congr1 parameters_poly_arr) + /last_poly_var_safe_poly_type [{}Hx]]. rewrite parameters_poly_arr_safe_poly_type /=. case: ts Hss; last done. move=> /= + ?. subst x ss. move=> /Forall_inv. rewrite subst_poly_type_poly_var. by move=> /generalize_GammaC /encodes_nat_transport H _ /H {}H _ /H{H} ->. } case. { move=> /[dup] [/(congr1 parameters_poly_arr) + /last_poly_var_safe_poly_type [{}Hx]]. rewrite parameters_poly_arr_safe_poly_type /=. case: ts Hss; last done. move=> /= + ?. subst x ss. move=> /Forall_inv. rewrite subst_poly_type_poly_var. by move=> /generalize_GammaC /encodes_nat_transport H /H {}H _ _ /H{H} ->. } by do 4 (case; first by move=> /last_poly_var_safe_poly_type [] ?; subst x). 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