proposition: Lemma G_not_in_F x y z E: ~ G x y z ∈ Fs E.
proof: Proof. intros (a & []) % in_Fs. eapply disjoint_F_G; eauto. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)