proposition: Lemma geneq_sym s (x: Term sign A s): ∀ s' (y: Term sign A s'), geneq x y → geneq y x.
proof: Proof. Proof with intuition. induction x. destruct y... simpl. symmetry... destruct y0... simpl in *... destruct y... simpl in *... Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.monads