proposition: Theorem addEqInclState2 : forall (S : State) (a b c d : rZ), inclState S (addEq (a, b) (addEq (c, d) S)).
proof: Proof. intros S a b c d. apply inclStateTrans with (S2 := addEq (c, d) S); auto with stalmarck. Qed.
imports: Coq(List)