symm
tactic #
This implements the symm
tactic, which can apply symmetry theorems to either the goal or a
hypothesis.
Environment extensions for symm lemmas
Given a term e : a ~ b
, construct a term in b ~ a
using @[symm]
lemmas.
Equations
Instances For
Apply a symmetry lemma (i.e. marked with @[symm]
) to a metavariable.
The type of g
should be of the form a ~ b
, and is used to index the symm lemmas.
Equations
Instances For
For every hypothesis h : a ~ b
where a @[symm]
lemma is available,
add a hypothesis h_symm : b ~ a
.