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