{ intro hast
  cases hast
  simp [*] }
case mp
B : State → Prop
s t : State
⊢ (Stmt.assert B, s) ⟹ t → t = s ∧ B s

case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t
case mpr
B : State → Prop
s t : State
⊢ t = s ∧ B s → (Stmt.assert B, s) ⟹ t