proposition: Theorem InRestrictState : forall (S : State) (L : list rNat) (a b : rZ), eqStateRz (restrictState S L) a b -> a <> b -> ~ contradictory S -> In (valRz a) L /\ In (valRz b) L.
proof: Proof. intros S L a b H' H'0 H'1. apply InState with (S := restrictState S L); auto with stalmarck. 2: assert (H'3:=restrictContradiction S L); red in H'3; auto with stalmarck. 2: red in |- *; intros H'2; apply H'1; auto with stalmarck. 2: Elimc H'3; intros H'3 H'4; lapply H'4; clear H'4; [ intros H'4; apply H'4 | idtac ]; auto with stalmarck. intros a0 b0; unfold restrictState in |- *. case (eqStateRzContrDec S); auto with stalmarck. intros H'2; case H'1; auto with stalmarck. red in |- *; exists rZTrue; auto with stalmarck. intros H'2 H'3; split. apply stripInRzIn1 with (L1 := stripRz S); auto with stalmarck. apply prodRzInL with (b := b0) (L2 := stripInRz L (stripRz S)); auto with stalmarck. apply stripRzDecProp1 with (S1 := S); auto with stalmarck. apply stripInRzIn1 with (L1 := stripRz S); auto with stalmarck. apply prodRzInR with (a := a0) (L1 := stripInRz L (stripRz S)); auto with stalmarck. apply stripRzDecProp1 with (S1 := S); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)