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