inductive World : Type

• w1: World
• w2: World
• w3: World

def example_frame : KripkeFrame

Equations

• example_frame = { W := World, R := fun (w₁ w₂ : World) => w₁ = World.w1 ∧ w₂ = World.w2 ∨ w₁ = World.w2 ∧ w₂ = World.w3 ∨ w₁ = World.w3 ∧ w₂ = World.w1 }