proposition: Theorem eqConstrStateInDouble : forall (S : State) (a b : rZ), eqConstrState S a b -> a <> b -> ~ (forall a b : rZ, eqStateRz S a b) -> In (a, b) (prodRz (stripRz S) (stripRz S)).
proof: Proof. intros S a b H' H'0 H'1. apply prodRzProp; auto with stalmarck. apply eqConstrStateInL with (b := b); auto with stalmarck. apply eqConstrStateInR with (a := a); auto with stalmarck. Qed.
imports: Coq(List)