absurd
and
and.elim_left
and.elim_right
and.intro
bool
bool.ff
bool.tt
char
char.mk
congr
dite
empty
empty.rec
eq
eq.elim_inv_inv
eq.intro
eq.rec
eq_rec_eq
eq.refl
eq.symm
eq.trans
exists.elim
false
false.rec
heq
heq.refl
heq.to_eq
iff
iff.refl
iff_false_intro
iff_true_intro
implies
implies_of_if_pos
implies_of_if_neg
ite
lift
lift.down
lift.up
nat
nat.of_num
nat.succ
nat.zero
not
num
num.zero
num.pos
option
option.some
option.none
or
or.elim
or.intro_left
or.intro_right
pos_num
pos_num.one
pos_num.bit0
pos_num.bit1
prod
prod.mk
prod.pr1
prod.pr2
propext
sigma
sigma.mk
string
string.empty
string.str
tactic
tactic.all_goals
tactic.apply
tactic.assert_hypothesis
tactic.eapply
tactic.fapply
tactic.eassumption
tactic.and_then
tactic.append
tactic.assumption
tactic.at_most
tactic.beta
tactic.builtin
tactic.cases
tactic.change
tactic.check_expr
tactic.clear
tactic.clears
tactic.determ
tactic.discard
tactic.intro
tactic.intros
tactic.exact
tactic.expr
tactic.expr.builtin
tactic.expr_list
tactic.expr_list.cons
tactic.expr_list.nil
tactic.using_expr
tactic.none_expr
tactic.identifier
tactic.identifier_list
tactic.opt_expr
tactic.opt_identifier_list
tactic.fail
tactic.fixpoint
tactic.focus_at
tactic.generalize_tac
tactic.generalizes
tactic.id
tactic.interleave
tactic.lettac
tactic.now
tactic.opt_expr_list
tactic.or_else
tactic.par
tactic.refine
tactic.rename
tactic.repeat
tactic.revert
tactic.reverts
tactic.rexact
tactic.rotate_left
tactic.rotate_right
tactic.state
tactic.trace
tactic.try_for
tactic.whnf
trans_rel_left
trans_rel_right
true
true.intro
is_trunc
is_trunc.trunc_index.of_nat
unit
unit.star
well_founded