proposition: Theorem RealizableCstr : forall (S : State) (i j : rZ), ~ eqStateRz S i j -> exists f : rNat -> bool, realizeState f S /\ negb (rZEval f i) = rZEval f j.
proof: Proof. intros S i j Hij; elim (Realizable S); [ intros f Pf | idtac ]. case (eqStateRzDec S (rZComp j) i); intros Hij'. exists f; split; auto with stalmarck; rewrite (realizeStateInvComp f S Pf j i); auto with stalmarck; rewrite <- (rZCompInv j); auto with stalmarck. case (EqboolDec (rZEval f i) (rZEval f j)); intros Fij. exists (fnAux S f i); split; auto with stalmarck; [ apply RealizableAux3 | rewrite (RealizableAux1 S f i i); auto with stalmarck; rewrite (RealizableAux2 S f i j) ]; auto with stalmarck. rewrite Fij; case (rZEval f j); simpl in |- *; auto with stalmarck. exists f; split; auto with stalmarck. red in |- *; intros Contr; elim Contr; intros a Pa; absurd (eqStateRz S i j); auto with stalmarck; apply eqStateRzContr with (a := a); auto with stalmarck. Qed.