Chapter 7. Tactics

Table of Contents

Quick reference card
absurd
apply
applyS
assumption
auto
cases
clear
clearbody
compose
change
constructor
contradiction
cut
decompose
demodulate
destruct
elim
elimType
exact
exists
fail
fold
fourier
fwd
generalize
id
intro
intros
inversion
lapply
left
letin
normalize
reflexivity
change
rewrite
right
ring
simplify
split
subst
symmetry
transitivity
unfold
whd

Quick reference card