proposition: Lemma G_injective a b c x y z: G a b c = G x y z -> a = x /\ b = y /\ c = z.
proof: Proof. intros H; unfold G in H; eapply injective_I__S in H. injection H as H. apply injective_I__P in H; injection H as ? H. apply injective_I__P in H; injection H as ? H. intuition. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)