The Coq mailing list

["fengsheng" <fsheng1990 AT 163.com>]

Error:
In environment
H : forall st st' : state, pXY / st || st' <-> pYX / st || st'
st : state
Heqst : st = empty_state
st1 : state
Heqst1 : st1 = update (update empty_state X 0) Y 2
H1 : pYX / st || st1
st2 : state
Heqst2 : st2 = update (update empty_state Y 0) X 0
H2 : pYX / st || st2
The term "pYX" has type "com" while it is expected to have type "Imp.com".

When I try to proof that st1 = st2, it just didnt do that and give the error
information above. What does that mean and how to solve it ?