Close the given goal if `h`

is a proof for an equality such as `as = a :: as`

.
Inductive datatypes in Lean are acyclic.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

def
Lean.MVarId.acyclic.go
(mvarId : Lean.MVarId)
(h : Lean.Expr)
(lhs : Lean.Expr)
(rhs : Lean.Expr)
:

## Equations

- One or more equations did not get rendered due to their size.