proposition: Theorem restrictContradiction : forall (S : State) (L : list rNat), contradictory S <-> contradictory (restrictState S L).
proof: Proof. intros S L; red in |- *; split; auto with stalmarck. unfold restrictState in |- *; case (eqStateRzContrDec S); auto with stalmarck. intros H' H'0; red in |- *; exists rZTrue; auto with stalmarck; auto with stalmarck. intros H' H'0; case H'; red in H'0. Elimc H'0; intros a E. intros a0 b; apply eqStateRzContr with (a := a); auto with stalmarck. intros H'; red in H'. Elimc H'; intros a E. red in |- *; exists a; auto with stalmarck. apply eqStateIncl with (S1 := restrictState S L); auto with stalmarck. apply restrictStateIncl; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)