apply BigStep.if_true
case mpr.while_true
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
case mpr.while_true.hcond
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ B s

case mpr.while_true.hbody
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (S; Stmt.whileDo B S, s) ⟹ t