# equation

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 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.

# cong

This meta implements the congruence closure algorithm. For example, given assumptions x = x’ and y = y’, it can prove f x y = f x’ y’.