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