proposition: Theorem inclStateAddEq : forall (S1 S2 : State) (a b : rZ), inclState S1 S2 -> inclState (addEq (a, b) S1) (addEq (a, b) S2).
proof: Proof. intros S1 S2 a b H'. apply inclStateAddEqInv; simpl in |- *. apply inclStateTrans with (S2 := S2); auto with stalmarck. apply eqStateRzIn; auto with stalmarck. simpl in |- *. auto with stalmarck. Qed.
imports: Coq(List)