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