proposition: Theorem eqStateEqEvalZ : forall (Ar : rArray vM) (S : State) (q r : rZ), wellFormedArray Ar -> rArrayState Ar S -> eqState (addEq (evalZ Ar q, evalZ Ar r) S) (addEq (q, r) S).
proof: Proof. intros Ar S q r H' H'0. apply eqStateEq1; auto with stalmarck. apply eqStateEvalZ; auto with stalmarck. apply eqStateEvalZ; auto with stalmarck. Qed.
imports: Stalmarck(interState doTriplet)