\
\(\*\*[^\)]
[^\(]\*\)
\(\*
\*\)
theorem
definition
lemma
fact
remark
variant
axiom
ntheorem
nrecord
ndefinition
ninductive
ncoinductive
nlet
nlemma
naxiom
alias
and
as
coercion
prefer
nocomposites
coinductive
corec
default
for
include
include'
inductive
inverter
in
interpretation
let
match
names
notation
on
qed
rec
record
return
source
to
using
with
unification
hint
ncoercion
ninverter
nqed
\[
\|
\]
\{
\}
@
\$
Set
Prop
Type
CProp
Prop
Type[0]
CProp[0]
Type[1]
CProp[1]
Type[2]
CProp[2]
absurd
apply
applyP
assumption
autobatch
cases
clear
clearbody
change
compose
constructor
contradiction
cut
decompose
destruct
elim
elimType
exact
exists
fail
fold
fourier
fwd
generalize
id
intro
intros
inversion
lapply
linear
left
letin
normalize
reflexivity
replace
rewrite
ring
right
symmetry
simplify
split
to
transitivity
unfold
whd
assume
suppose
by
is
or
equivalent
equivalently
we
prove
proved
need
proceed
induction
inductive
case
base
let
such
that
by
have
and
the
thesis
becomes
hypothesis
know
case
obtain
conclude
done
rule
napply
ncases
nletin
nauto
nelim
nwhd
nnormalize
nassumption
ngeneralize
nchange
nrewrite
ncut
nlapply
try
solve
do
repeat
first
focus
unfocus
progress
skip
inline
procedural
check
eval
hint
set
auto
nodefaults
coercions
comments
debug
cr
ncheck
elim
hint
instance
locate
match
def
forall
lambda
to
exists
Rightarrow
Assign
land
lor
lnot
liff
subst
vdash
iforall
iexists
"
"