proposition: Theorem restrictStateInZeroR : forall (S : State) (L : list rNat) (a b : rZ), In zero L -> In (a, b) (restrictState S L) -> In (valRz b) L.
proof: Proof. intros S L a b H'; unfold restrictState in |- *. case (eqStateRzContrDec S); simpl in |- *; auto with stalmarck. intros H'0 H'1; Elimc H'1; intros H'1; inversion H'1; auto with stalmarck. intros H'0 H'1. apply stripInRzIn1 with (L1 := stripRz S); auto with stalmarck. apply prodRzInR with (a := a) (L1 := stripInRz L (stripRz S)); auto with stalmarck. apply stripRzDecProp1 with (S1 := S); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)