proposition: Lemma RealizableAux2 : forall (S : State) (f : rNat -> bool) (i j : rZ), ~ eqStateRz S j i -> ~ eqStateRz S (rZComp j) i -> rZEval (fnAux S f i) j = rZEval f j.
proof: Proof. simple destruct j; intros n Eq1 Eq2; unfold fnAux in |- *; simpl in |- *; case (eqStateRzDec S (rZPlus n) i); case (eqStateRzDec S (rZMinus n) i); auto with stalmarck; intros; (absurd (eqStateRz S (rZPlus n) i); auto with stalmarck; fail) || absurd (eqStateRz S (rZMinus n) i); auto with stalmarck. Qed.