pub fn normalize_s5(expr: &TLExpr) -> TLExpr
Normalize a modal expression according to S5 axioms.
In S5, any sequence of modal operators can be reduced to a single operator. This function reduces nested modalities.