• Summary of the discussion:
• Recursors/Eliminators of inductive types
• Guardedness predicate
• Well-founded relations
• Sized Types
• References