apply Exists.intro t
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ ∃ t, B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u
case mp.while_true.h
B : State → Prop
S : Stmt
s u t : State
hB : B s
hS : (S, s) ⟹ t
hw : (Stmt.whileDo B S, t) ⟹ u
⊢ B s ∧ (S, s) ⟹ t ∧ (Stmt.whileDo B S, t) ⟹ u