• File Structure
• Layout
• Layout of Proofs
• Naming
• Lemmas and Data-types
• Variables inside proofs
• Extraction