Introduction

• Conventions
• Universes and Level Expressions
• Formula Structure
• Soft Abstractions
• The Sequent
• Proof Annotations
  • Goal Labels
  • Tactic Arguments
• Matching and Substitution