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