proposition: Theorem eqConstrStateInL : forall (S : State) (a b : rZ), eqConstrState S a b -> a <> b -> ~ (forall a b : rZ, eqStateRz S a b) -> In a (stripRz S).
proof: Proof. intros S a b H'; Elimc H'; clear S a b; auto with stalmarck; simpl in |- *. intros a H'0; case H'0; auto with stalmarck. intros a b p; case p; intros a' b'; simpl in |- *; auto with stalmarck. intros S H' H'0 H'1 H'2; right; right; right; right; auto with stalmarck. intros a b c d S H' H'0 H'1 H'2 H'3 H'4. case (rZDec a b); intros Eq1; auto with stalmarck. right; right; right; right; auto with stalmarck. intros a b c d S H' H'0 H'1 H'2 H'3 H'4. case (rZDec a c); intros Eq1; auto with stalmarck. right; right; right; right; auto with stalmarck. intros a b c d S H' H'0 H'1 H'2 H'3 H'4. case (rZDec a (rZComp b)); intros Eq1; auto with stalmarck. right; right; right; right; auto with stalmarck. intros a b c d S H' H'0 H'1 H'2 H'3 H'4. case (rZDec a (rZComp c)); intros Eq1; auto with stalmarck. right; right; right; right; auto with stalmarck. intros a b c d S H' H'0 H'1 H'2. case H'2; intros a0 b0. apply eqStateRzContr with (a := b); auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. Qed.
imports: Coq(List)