proposition: Theorem realizeStateAddEq : forall (f : rNat -> bool) (S : State), realizeState f S -> forall i j : rZ, rZEval f i = rZEval f j -> realizeState f (addEq (i, j) S).
proof: Proof. intros f S H' i j H'0; red in |- *; simpl in |- *; auto with stalmarck. intros i0 j0 H'1; elim H'1; intros H'2; clear H'1; [ inversion H'2 | idtac ]; auto with stalmarck. rewrite <- H1; auto with stalmarck. rewrite <- H0; auto with stalmarck. Qed.
imports: Coq(List)