{- | `rewrite (p : a = b) t : T` replaces occurrences of `a` in `T` with a variable `x` obtaining a type `T[x/a]` and returns `transportInv (\lam x => T[x/a]) p t`

 - If the expected type is unknown, the meta rewrites in the type of the arguments instead.
 - `rewrite {i_1, ... i_k} p t` replaces only occurrences with indices `i_1`, ... `i_k`. Here `i_j` is the number of occurrence after replacing all the previous occurrences. 
 - Also, `p` may be a function, in which case `rewrite p` is equivalent to `rewrite (p _ ... _)`.
 - `rewrite (p_1, ... p_n) t` is equivalent to `rewrite p_1 (... rewrite p_n t ...)`

 -}
\meta rewrite

-- | `rewriteI p` is equivalent to `rewrite (inv p)`
\meta rewriteI

{- | `rewriteEq (p : a = b) t : T` is similar to {rewrite}, but it finds and replaces occurrences of `a` up to algebraic equivalences.
 - For example, `rewriteEq (p : b * (c * id) = x) t : T` rewrites `(a * b) * (id * c)` as `a * x` in `T`. 
 - Similarly to `rewrite` this meta allows specification of occurrence numbers. 
 - Currently this meta supports noncommutative monoids and categories.

 -}
\meta rewriteEq

-- | Simplifies the expected type or the type of the argument if the expected type is unknown.
\meta simplify

{- | Simplifies certain equalities. It expects one argument and the type of this argument is called 'subgoal'. The expected type is called 'goal'.
 - * If the goal is `coe (\lam i => \Pi (x : A) -> B x i) f right a = b'`, then the subgoal is `coe (B a) (f a) right = b`.
 - * If the goal is `coe (\lam i => \Pi (x : A) -> B x i) f right = g'`, then the subgoal is `\Pi (a : A) -> coe (B a) (f a) right = g a`.
 - * If the goal is `coe (\lam i => A i -> B i) f right = g'`, then the subgoal is `\Pi (a : A left) -> coe B (f a) right = g (coe A a right)`.
 - * If the type under `coe` is a higher-order non-dependent function type, `simp_coe` simplifies it recursively.
 - * If the goal is `(coe (\lam i => \Sigma (x_1 : A_1 i) ... (x_n : A_n i) ...) t right).n = b'`, then the subgoal is `coe A_n t.n right = b`.
 - * If the goal is `coe (\lam i => \Sigma (x_1 : A_1) ... (x_n : A_n) (B_{n+1} i) ... (B_k i)) t right = s'`, then the subgoal is a \Sigma type consisting of equalities as specified above ignoring fields in \Prop.
 - * If the type under `coe` is a record, then `simp_coe` works similarly to the case of \Sigma types. The copattern matching syntax as in {ext} is also supported.
 - * All of the above cases also work for goals with {transport} instead of {coe} since the former evaluates to the latter.
 - * If the goal is `transport (\lam x => f x = g x) p q = s`, then the subgoal is `q *> pmap g p = pmap f p *> s`. If `f` does not depend on `x`, then the right hand side of the subgoal is simply `s`.
 - If the expected type is unknown or if the meta is applied to more than one argument, then it applies to the type of the argument instead of the expected type.

 -}
\meta simp_coe

{- | Proves goals of the form `a = {A} a'`. It expects (at most) one argument and the type of this argument is called 'subgoal'. The expected type is called 'goal'
 - * If the goal is `f = {\Pi (x_1 : A_1) ... (x_n : A_n) -> B} g`, then the subgoal is `\Pi (x_1 : A_1) ... (x_n : A_n) -> f x_1 ... x_n = g x_1 ... x_n`
 - * If the goal is `t = {\Sigma (x_1 : A_1) ... (x_n : A_n) (y_1 : B_1 x_1 ... x_n) ... (y_k : B_k x_1 ... x_n) (z_1 : C_1) ... (z_m : C_m)} s`, where `C_i : \Prop` and they can depend on `x_j` and `y_l` for all `i`, `j`, and `l`, then the subgoal is `\Sigma (p_1 : t.1 = s.1) ... (p_n : t.n = s.n) D_1 ... D_k`, where `D_j` is equal to `coe (\lam i => B (p_1 @ i) ... (p_n @ i)) t.{k + j - 1} right = s.{k + j - 1}`
 - * If the goal is `t = {R} s`, where `R` is a record, then the subgoal is defined in the same way as for \Sigma-types It is also possible to use the following syntax in this case: `ext R { | f_1 => e_1 ... | f_l => e_l }`, which is equivalent to `ext (e_1, ... e_l)`
 - * If the goal is `A = {\Prop} B`, then the subgoal is `\Sigma (A -> B) (B -> A)`
 - * If the goal is `A = {\Type} B`, then the subgoal is `Equiv {A} {B}`
 - * If the goal is `x = {P} y`, where `P : \Prop`, then the argument for {ext} should be omitted

 -}
\meta ext

-- | Similar to {ext}, but also applies either {simp_coe} or {ext} when a field of a \Sigma-type or a record has an appropriate type.
\meta exts