fact: Definition G (x y z: nat): nat := I__S (inr (I__P (x, I__P (y, z)))).
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)