proposition: Theorem interMemInL : forall S1 S2 : State, inclState (interState S1 S2) S1.
proof: Proof. intros S1 S2; unfold interState in |- *. case (eqStateRzContrDec S1); auto with stalmarck. intros H'; apply inclStateIn; auto with stalmarck. intros H'; apply inclStateIn; auto with stalmarck. intros a b H'1. apply eqConstrStateImpeqStateRz. apply stripRzDecProp2 with (S2 := prodRz (stripRz S1) (stripRz S1)); auto with stalmarck. apply stripRzDecProp1 with (S1 := S2); auto with stalmarck. Qed.
imports: Coq(List)