Namespace derive and satisfies

[madvorak]

I don't think that derive and satisfies should be declared in the global namespace.

equational_theories/equational_theories/MagmaLaw.lean

Line 46 in bfcc12a

inductive derive.{u} {α : Type u} (Γ : Ctx α) : MagmaLaw α → Type u where

equational_theories/equational_theories/MagmaLaw.lean

Line 90 in bfcc12a

def satisfies {α} (G) [Magma G] (E : MagmaLaw α) := ∀ (φ : α → G), satisfiesPhi φ E

I suggest MagmaLaw.derive and MagmaLaw.satisfies as better names.

PS: I don't see a point of MagmaLaw being inside Law itself. However, it is another story.

[teorth]

Provided that the refactor can be done easily, I have no objection to this change.