proposition: Lemma transport : forall c, In c upcs -> h10upc_sem φ' c.
proof: Proof. Proof using Hφ. apply /Forall_forall /Forall_flat_map. move: Hφ => /Forall_forall. apply: Forall_impl => - [[x y] z] /= ?. constructor; [|constructor; [|constructor]]; last done. all: rewrite /φ' /= ?Cantor.cancel_of_to ?(c2_spec _); lia. Qed.
imports: List Lia Cantor ssreflect ssrbool ssrfun Undecidability.DiophantineConstraints.H10C