proposition: Theorem interMemProp : forall S1 S2 : State, interStateP S1 S2 (interState S1 S2).
proof: Proof. intros S1 S2; repeat split; auto with stalmarck. intros S4 H1 H2; red in |- *; intros i j H3. apply interMemEqStateRz; auto with stalmarck. Qed.
imports: Coq(List)