# Glossary

a | b | c | d | e | f | g | h | i | l | n | 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 cone expression constant context-local definition contraction convertible d de Bruijn criterion definitional equality delta-reduction dependent premise dependent product e equality eta-expansion existential variable expansion f field first success flag forward reasoning g global environment goal h head head constant hypothesis i implicit argument induction principle inductive parameter inductively defined proposition inhabited iota-reduction l left associative Leibniz equality local context n non-dependent premise o occurrence opaque option p prelude premise product projection proof mode proof state proof term proposition q quotient quotient set r records reduction reversible coercion right associative s sentence setoid setoid equality shelved sort standard library strict proposition subgoal t table tactic term transparent type u unfold uniform inheritance condition unshelved w weak-head normal form well-typed witness z zeta-reduction