constructor
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q ↔ p = q
case mp
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ mop i p = mop i q → p = q

case mpr
ι : Type u_2
F : Type u_1
inst✝ : UnaryModalOperator ι F
i : ι
p q : F
⊢ p = q → mop i p = mop i q