proposition: Theorem restrictStateInvol : forall (S : State) (L : list rNat), In zero L -> eqState (restrictState S L) (restrictState (restrictState S L) L).
proof: Proof. intros S L H; red in |- *; split; auto with stalmarck. 2: apply restrictStateIncl; auto with stalmarck. apply inclStateIn; auto with stalmarck. intros a b H'. apply restrictStateComp; auto with stalmarck. apply restrictStateInZeroL with (S := S) (b := b); auto with stalmarck. apply restrictStateInZeroR with (S := S) (a := a); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)