proposition: Theorem addEqUnion : forall (S : State) (p q : rZ), unionStateP ((p, q) :: nil) S (addEq (p, q) S).
proof: Proof. intros S p q. apply unionStatePDef; auto with stalmarck. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a b H'; elim H'; intros H'0; inversion H'0; auto with stalmarck. Qed.
imports: Coq(List)