• Can you explain me what an evaluable constant is?
• What is a goal?
• What is a meta variable?
• What is Gallina?
• What is The Vernacular?
• What is a dependent type?
• What is a proof by reflection?
• What is intuitionistic logic?
• What is proof-irrelevance?
• What is the difference between opaque and transparent?
• References