proposition: Lemma in_Fs y E: y ∈ Fs E -> exists x, F x = y /\ x ∈ Vars__de E.
proof: Proof. intros H; unfold Fs in *; now eapply in_map_iff in H. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)