proposition: Theorem restrictEqComp : forall (S1 S2 : State) (L : list rNat), eqState S1 S2 -> eqState (restrictState S1 L) (restrictState S2 L).
proof: Proof. intros S1 S2 L H'; red in |- *; split; apply restricMonotone; auto with datatypes stalmarck; red in H'; elim H'; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)