apply Or.intro_right
case mp.if_false
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hT : (T, s) ⟹ t
⊢ B s ∧ (S, s) ⟹ t ∨ ¬B s ∧ (T, s) ⟹ t
case mp.if_false.h
B : State → Prop
S T : Stmt
s t : State
hB : ¬B s
hT : (T, s) ⟹ t
⊢ ¬B s ∧ (T, s) ⟹ t