proposition: Theorem eqStateTrans : forall S1 S2 S3 : State, eqState S1 S2 -> eqState S2 S3 -> eqState S1 S3.
proof: Proof. intros S1 S2 S3 H' H'0; inversion H'; inversion H'0. red in |- *; split; apply inclStateTrans with (S2 := S2); auto with stalmarck. Qed.
imports: Coq(List)