Reserved Notation "φ₁ →→ φ₂" (at level 11, right associativity).
Reserved Notation "a '⊢ᴛy' b : c" (at level 20, b at level 99, c at level 80).
Reserved Notation "a '⊢ᴄᴏ' b : c ∼ d" (at level 20, b at level 99).
Reserved Notation "Γ '+' x : c" (at level 50, x at level 99).
Reserved Notation "Γ '++' x : a ∼ b" (at level 50, x at level 99).
Reserved Notation "φ₁ →→ φ₂" (at level 11, right associativity).
Reserved Notation "a '⊢ᴛy' b : c" (at level 20, b at level 99, c at level 80).
Reserved Notation "a '⊢ᴄᴏ' b : c ∼ d" (at level 20, b at level 99).
Reserved Notation "Γ '+' x : c" (at level 50, x at level 99).
Reserved Notation "Γ '++' x : a ∼ b" (at level 50, x at level 99).