constructor
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~⌈∗β⌉ψ) ↔ evaluate M w ρ
case mp
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~⌈∗β⌉ψ) → evaluate M w ρ

case mpr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)