α
slide: Behavioral subtyping constraints