proposition: Lemma inverse_transport : forall c, In c ucs -> h10uc_sem φ c.
proof: Proof. Proof using Hφ'. apply /Forall_forall. move: Hφ' => /Forall_forall /Forall_flat_map. apply: Forall_impl => - [[x y] z] /=. move=> /Forall_cons_iff [+] /Forall_cons_iff [+] /Forall_cons_iff [+ _]. rewrite /φ /=. nia. Qed.
imports: List Lia Cantor ssreflect ssrbool ssrfun Undecidability.DiophantineConstraints.H10C