proposition: Lemma h10sqc_to_h10ucs_spec {c} : h10sqc_sem φ c -> Forall (h10uc_sem φ') (h10sqc_to_h10ucs c).
proof: Proof. case: c => /=. - move=> x ?. constructor; last done. rewrite /= /ζ /φ' /v ?Cantor.cancel_of_to /=. by lia. - move=> x y z ?. (do ? constructor); rewrite /= /ζ /φ' /θ ?Cantor.cancel_of_to /=; by nia. - move=> x y ?. (do ? constructor); rewrite /= /ζ /φ' ?Cantor.cancel_of_to /=; by nia. Qed.
imports: List Lia Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun