proposition: Lemma Gs_in x y z E: (x *ₑ y =ₑ z) ∈ E -> G x y z ∈ Gs E.
proof: Proof. intros; eapply in_flat_map. exists (x *ₑ y =ₑ z). intuition (auto with datatypes). Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)