apply And.intro <;>
  assumption
case mp.seq.h
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ (S, s) ⟹ ?mp.seq.w ∧ (T, ?mp.seq.w) ⟹ u

case mp.seq.w
S T : Stmt
s u t✝ : State
hS✝ : (S, s) ⟹ t✝
hT✝ : (T, t✝) ⟹ u
⊢ State
no goals