proposition: Theorem restrictStateComp : forall (S : State) (L : list rNat) (a b : rZ), In (valRz a) L -> In (valRz b) L -> eqStateRz S a b -> eqStateRz (restrictState S L) a b.
proof: Proof. intros S L a b H' H'0 H'1. unfold restrictState in |- *. case (eqStateRzContrDec S). intros H'2. apply eqStateRzContr with (a := rZTrue); auto with stalmarck. intros H'2. case (rZDec a b). intros H'3; rewrite H'3; auto with stalmarck. intros H'3. apply eqStateRzIn; auto with stalmarck. apply stripRzDecProp3; auto with stalmarck. apply prodRzProp; auto with stalmarck. apply stripInRzIn; auto with stalmarck. apply eqConstrStateInL with (b := b); auto with stalmarck. apply stripInRzIn; auto with stalmarck. apply eqConstrStateInR with (a := a); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)