{- | `equation a_1 ... a_n` proves an equation a_0 = a_{n+1} using a_1, ... a_n as intermediate steps

 - A proof of a_i = a_{i+1} can be specified as implicit arguments between them.
 - `using`, `usingOnly`, and `hiding` with a single argument can be used instead of a proof to control the context.
 - The first implicit argument can be either a universe or a subclass of either {Algebra.Monoid.Monoid}, {Algebra.Monoid.AddMonoid}, or {Order.Lattice.Bounded.MeetSemilattice}.
 - In the former case, the meta will prove an equality in a type without using any additional structure on it.
 - In the latter case, the meta will prove an equality using only structure available in the specified class.

 -}
\meta equation

-- | Solve systems of linear equations
\meta linarith

-- | Proves an equality by congruence closure of equalities in the context. E.g. derives f a = g b from f = g and a = b
\meta cong