proposition: Theorem unionStateAssoc : forall S1 S2 S3 : State, eqState (unionState S1 (unionState S2 S3)) (unionState (unionState S1 S2) S3).
proof: Proof. intros S1 S2 S3; red in |- *; split. apply unionStateMin; auto with stalmarck. apply inclStateTrans with (S2 := unionState S1 S2); auto with stalmarck. apply unionStateMin; auto with stalmarck. apply inclStateTrans with (S2 := unionState S1 S2); auto with stalmarck. apply unionStateMin; auto with stalmarck. apply unionStateMin; auto with stalmarck. apply inclStateTrans with (S2 := unionState S2 S3); auto with stalmarck. apply inclStateTrans with (S2 := unionState S2 S3); auto with stalmarck. Qed.
imports: Coq(List)