apply Iff.intro
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t ↔ (Stmt.skip, s) ⟹ t
case mp
x : String
s t : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ t → (Stmt.skip, s) ⟹ t

case mpr
x : String
s t : State
⊢ (Stmt.skip, s) ⟹ t → (Stmt.assign x fun s => s x, s) ⟹ t