Function apply_kripke_lowering 

pub fn apply_kripke_lowering<'a>(
    expr: &'a LogicExpr<'a>,
    expr_arena: &'a Arena<LogicExpr<'a>>,
    term_arena: &'a Arena<Term<'a>>,
    interner: &mut Interner,
) -> &'a LogicExpr<'a>

Apply Kripke lowering to transform modal operators into explicit world quantification.

This transforms surface modal operators (◇, □) into explicit First-Order Logic with possible world semantics, enabling Z3 verification.

Example

Surface: ◇Fly(x) (John can fly) Deep: ∃w'(Accessible(w₀, w') ∧ Fly(x, w')) (There exists an accessible world where John flies)