Rocq studies

rewrite-rules

• L01_Conversion.v
• L02_Patterns.v
• L03_Admission.v
• L04_Boundaries.v
• L05_Triangle.v

termination

• Euclid.v
• L01_Baseline.v
• L02_Obligations.v
• L03_Accessibility.v
• L04_Admission.v