proposition: Theorem interMemMin : forall S1 S2 S3 : State, inclState S3 S1 -> inclState S3 S2 -> inclState S3 (interState S1 S2).
proof: Proof. intros S1 S2 S3 H' H'0. assert (H'2 := interMemProp S1 S2). apply (interStatePIncl S1 S2); auto with stalmarck. Qed.
imports: Coq(List)