";"	Imp:Coq Automation:Tacticals:The ; Tactical (General Form)
";" (general form)	Imp:Coq Automation:Tacticals:The ; Tactical (General Form)
"_"	Basics:Enumerated Types:Numbers
"as" clause	Basics:Proof by Case Analysis
abstract syntax	Imp:Arithmetic and Boolean Expressions:Syntax
admit	Basics:Enumerated Types:Booleans
admit (Definition)	Basics:Enumerated Types:Booleans
Admitted	Basics:Enumerated Types:Booleans
Admitted (Definition)	Basics:Enumerated Types:Booleans
Apply (Proposition)	Prop:Inductively Defined Propositions:Inference Rules:
Assertion (definition)	Hoare:Hoare Logic:Assertions
Assignment Rule for Hoare Triples	Hoare:Hoare Logic:Proof Rules:Assignment
assumption	Imp:Coq Automation:A Few More Handy Tactics
automation	Imp:Coq Automation
bassn (lifting bexp to assertions)	Hoare:Hoare Logic:Proof Rules:Conditionals
beautfiul (Inference Rules)	Prop:Inductively Defined Propositions:Example
beautiful (Definition)	Prop:Inductively Defined Propositions:Inference Rules:
beautiful (Proposition)	Prop:Inductively Defined Propositions:?:Discussion: Computational vs. Inductive Definitions
Biconditional (Definition)	Logic:Iff
Biconditional (Example)	Logic:Iff
Check	Basics:Enumerated Types:Function Types
clear	Imp:Coq Automation:A Few More Handy Tactics
compute	Basics:Enumerated Types:Numbers
compute	Basics:Enumerated Types:Numbers
Conditional Rule for Hoare Triples	Hoare:Hoare Logic:Proof Rules:Conditionals
Conjunction (Definition)	Logic:Conjunction (Logical "and")
Conjunction (Example)	Logic:Conjunction (Logical "and"):"Introducing" Conjuctions
Conjunction (Example)	Logic:Conjunction (Logical "and"):"Eliminating" conjunctions
Consequence Rules for Hoare Triples	Hoare:Hoare Logic:Proof Rules:Consequence
Constructor	Basics:Enumerated Types:Numbers
constructor	Imp:Coq Automation:A Few More Handy Tactics
Context	Basics:Proof by Simplification
contradiction	Imp:Coq Automation:A Few More Handy Tactics
Decorated Program	Hoare:Hoare Logic:Proof Rules:Sequencing
Definition (First use)	Basics:Enumerated Types:Days of the Week
destruct	Basics:Proof by Case Analysis
determinism (evaluation)	Imp:Evaluation:Determinism of Evaluation
Disjunction (Definition)	Logic:Disjunction (Logical "or"):Implementing Disjunction
Disjunction (Example)	Logic:Disjunction (Logical "or"):Implementing Disjunction:
eapply (tactic)	Hoare:Hoare Logic:Proof Rules:Digression: The eapply Tactic
ev (Definition)	Prop:Inductively Defined Propositions:Inference Rules:
Eval	Basics:Enumerated Types:Numbers
evaluation (arithmetic/boolean expressions)	Imp:Arithmetic and Boolean Expressions:Evaluation
evaluation relation	Imp:Evaluation:Evaluation as a Relation
evaluation relation	Imp:Evaluation:Evaluation as a Relation
even (Definition)	Prop:From Boolean Functions to Propositions
ex falso quodlibet	Logic:Falsehood:?:
Example	Basics:Enumerated Types:Days of the Week
Extraction	Basics:Enumerated Types:Days of the Week
Fact	Basics:Proof by Simplification
Falsehood (Definition)	Logic:Falsehood
Fixpoint	Basics:Enumerated Types:Numbers
forall	Basics:Proof by Simplification
Function Types	Basics:Enumerated Types:Function Types
Goal	Basics:Proof by Simplification
gorgeous (Definition)	Prop:Inductively Defined Propositions:Induction Over Evidence:
Hoare Triple (definition)	Hoare:Hoare Logic:Hoare Triples
Implication and Iff for assertions (notation)	Hoare:Hoare Logic:Notation for Assertions
Implications (Example)	Logic:Proofs and Evidence:Implications are functions
Implications are functions	Logic:Proofs and Evidence:?:
Induction over Evidence	Prop:Inductively Defined Propositions:Inference Rules:
Inductive	Basics:Enumerated Types:Days of the Week
Inductive	Basics:Enumerated Types:Numbers
Inductive Definition	Basics:Enumerated Types:Numbers
Inequality (Definition)	Logic:Negation:Inequality
Inequality (Example)	Logic:Negation:Inequality
inference rules	Imp:Evaluation as a Relation:Inference Rule Notation
Inference Rules	Prop:Inductively Defined Propositions:Example
Inference Trees	Prop:Inductively Defined Propositions:Inference Rules:
intros	Basics:Proof by Simplification
Inversion on Evidence	Prop:Inductively Defined Propositions:Induction Over Evidence:
Inversion revisited	Prop:Inductively Defined Propositions:Inversion on Evidence:
le (Definition)	Prop:Relations
Lemma	Basics:Proof by Simplification
library import	Imp:Imp: Simple Imperative Programs:?:Sflib
Loop Rule for Hoare Triples	Hoare:Hoare Logic: So Far:Hoare Logic Rules (so far):
match	Basics:Enumerated Types:Days of the Week
match	Basics:Enumerated Types:Numbers
Module	Basics:Enumerated Types:Numbers
Natural Numbers	Basics:Enumerated Types:Numbers
Negation (Definition)	Logic:Negation
Negation (Example)	Logic:Negation:?:
Notation	Basics:Enumerated Types:Numbers
Notation	Basics:Optional Material:More on Notation
Notation (tactics)	Imp:Coq Automation:Defining New Tactic Notations
omega	Imp:Coq Automation:The omega Tactic
operational semantics	Imp:Evaluation:Evaluation as a Relation
Pattern Matching	Basics:Enumerated Types:Days of the Week
Proof Trees	Prop:Inductively Defined Propositions:Inference Rules:
proofs (Example)	Logic:Proofs and Evidence:?:
Proofs and evidence	Logic:Propositions
Proposition (Computational)	Prop:From Boolean Functions to Propositions
Proposition (Inductive)	Prop:Inductively Defined Propositions:Inference Rules:
Propositions	Logic:Logic: Logic in Coq
Propositions (Definition of)	Logic:Proofs and Evidence:Implications are functions
Propositions (Example)	Logic:Propositions
Propositions (Summary)	Prop:Relations:?:
Recursive Function	Basics:Enumerated Types:Numbers
reflexivity	Basics:Enumerated Types:Days of the Week
reflexivity	Basics:Proof by Simplification
Relations	Prop:Additional Exercises
Remark	Basics:Proof by Simplification
rename	Imp:Coq Automation:A Few More Handy Tactics
repeat	Imp:Coq Automation:Tacticals:The repeat Tactical
rewrite	Basics:Proof by Rewriting
Sequencing Rule for Hoare Triples	Hoare:Hoare Logic:Proof Rules:Sequencing
Sflib	Imp:Imp: Simple Imperative Programs:?:Sflib
simpl	Basics:Enumerated Types:Numbers
Simplification	Basics:Proof by Simplification
Skip Rule for Hoare Triples	Hoare:Hoare Logic:Proof Rules:Skip
Structural Recursion	Basics:Optional Material:Fixpoints and Structural Recursion
subst	Imp:Coq Automation:A Few More Handy Tactics
Substitution in Assertions (definition)	Hoare:???
syntax (arithmetic/boolean expressions)	Imp:Arithmetic and Boolean Expressions:Syntax
syntax (arithmetic/boolean expressions)	Imp:Expressions With Variables:Syntax
syntax (commands)	Imp:Commands:Syntax
tacticals	Imp:Coq Automation
Tactics	Basics:Proof by Simplification
Theorem	Basics:Proof by Simplification
Truth (Definition)	Logic:Falsehood:Truth
try	Imp:Coq Automation:Tacticals:The try Tactical
Type inference	Basics:Enumerated Types:Days of the Week
Wildcard Pattern	Basics:Enumerated Types:Numbers