proposition: Lemma transport : H10C_SAT cs -> H10SQC_SAT sqcs.
proof: Proof. move=> [φ Hφ]. exists (φ' φ). move: Hφ. rewrite -?Forall_forall /sqcs Forall_flat_map. apply: Forall_impl => ?. by move /h10c_to_h10sqcs_spec. Qed.
imports: List Lia Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun