fact: Fixpoint geneq {s s'} (x: Term sign A s) (y: Term sign A s'): Prop := match x, y with | Var _ _ v _, Var _ _ w _ => v = w | App _ _ _ z t t', App _ _ _ z' t'' t''' => geneq t t'' ∧ geneq t' t''' | Op _ _ o, Op _ _ o' => o ≡ o' | _, _ => False end.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.monads