API: Create an API to handle Magma words, equations, and implications as syntactic objects

[teorth]

See the discussion in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Syntax . Among other things, this would allow one to prove "metatheorems" about equations, for instance that the equation "x = f(y,z,w)" is equivalent to "x=y" for any word f.