proposition: Theorem interMemEqStateRz : forall (S1 S2 : State) (a b : rZ), eqStateRz S1 a b -> eqStateRz S2 a b -> eqStateRz (interState S1 S2) a b.
proof: Proof. intros S1 S2; unfold interState in |- *. case (eqStateRzContrDec S1); auto with stalmarck. intros H' a b H'0 H'1; case (rZDec a b); intros Eqab; auto with stalmarck. rewrite <- Eqab; auto with stalmarck. apply eqStateRzIn; auto with stalmarck. repeat apply stripRzDecProp3; auto with stalmarck. apply eqConstrStateInDouble; auto with stalmarck. Qed.
imports: Coq(List)