{- | `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