---

---

slide: Behavioral subtypes -- proof obligations

---