proposition: Lemma in_Equations q E: q ∈ Eqs E <-> (exists e, e ∈ E /\ q ∈ eqs e).
proof: Proof. eapply in_flat_map. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)