{ intro hseq
  cases hseq with
  | seq _ _ _ u _ hs hS =>
    cases hs
    assumption }
case mp
S : Stmt
s t : State
⊢ (Stmt.skip; S, s) ⟹ t → (S, s) ⟹ t

case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (Stmt.skip; S, s) ⟹ t
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (Stmt.skip; S, s) ⟹ t