proposition: Theorem restrictStateIncl : forall (S : State) (L : list rNat), inclState (restrictState S L) S.
proof: Proof. intros S L; unfold restrictState in |- *. case (eqStateRzContrDec S); auto with stalmarck. intros H'; red in |- *; auto with stalmarck. intros H'; apply inclStateIn; auto with stalmarck. intros a b H'0; apply eqConstrStateImpeqStateRz. apply stripRzDecProp2 with (S2 := prodRz (stripInRz L (stripRz S)) (stripInRz L (stripRz S))); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)