proposition: Lemma in_Gs y E: y ∈ Gs E -> exists a b c, G a b c = y /\ (a *ₑ b =ₑ c) ∈ E.
proof: Proof. intros H; unfold Gs in *; eapply in_flat_map in H. destruct H as [[]]; cbn in *; intuition. subst. exists x; exists y0; exists z. intuition. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)