# Glossary

a | b | c | d | e | f | g | h | i | l | o | p | q | r | s | t | u | w | z
 a algebraic universe alpha-convertible attribute b backtracking backtracking point backward reasoning beta-redex beta-reduction body boolean attribute branching c Calculus of Inductive Constructions command conclusion constant contraction convertible d de Bruijn criterion definitional equality delta-reduction e equality eta-expansion existential variable expansion f first success flag forward reasoning g global environment goal h head head constant hypothesis i inhabited iota-reduction l left associative Leibniz equality local context o occurrence opaque option p prelude proof mode proof state proof term proposition q quotient quotient set r reduction right associative s sentence setoid setoid equality shelved sort standard library strict proposition subgoal t table tactic term transparent type u unfold unshelved w weak-head normal form well-typed witness z zeta-reduction