proposition: Lemma encodes_nat_transport {s t n n'} : iipc2 GammaC (poly_arr (to_d s) (to_d t)) -> encodes_nat s n -> encodes_nat t n' -> n = n'.
proof: Proof. move=> + [Hn _] [_ Hn']. move: Hn => /iipc2_poly_arr_comp H /H{H}. move: Hn' => + /iipc2_poly_arr_comp H => /H{H} /iipc2_to_dE. rewrite /dt /zt /zt'. 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