proposition: Lemma disjoint_F_G x m n p: F x <> G m n p.
proof: Proof. intros H. unfold F, G in H; eapply injective_I__S in H. discriminate. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)