# Glossary

a | b | c | d | e | f | g | h | i | l | o | p | q | r | s | t | u | w
 a attribute alpha-convertible algebraic universe b boolean attribute branching backtracking backtracking point backward reasoning c command convertible conclusion d de Bruijn criterion definitional equality e existential variable equality f flag first success forward reasoning g goal global environment h hypothesis i inhabited l left associative local context Leibniz equality o option occurrence p prelude proposition proof mode proof state proof term q quotient set quotient r right associative s standard library sentence sort strict proposition subgoal shelved setoid equality setoid t term type tactic table u unshelved w well-typed witness