proposition: Lemma Fs_in x E: x ∈ Vars__de E -> F x ∈ Fs E.
proof: Proof. intros; eapply in_map_iff. exists x; intuition. Qed.
imports: RelationClasses Morphisms List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus second_order.diophantine_equations systemunification nth_order_unification)