proposition: Theorem RestrictAddEq : forall (S : State) (L : list rNat) (a b : rZ), In (valRz a) L -> In (valRz b) L -> In zero L -> eqState (restrictState (addEq (a, b) S) L) (addEq (a, b) (restrictState S L)).
proof: Proof. intros S L a b H' H'0 H'1; red in |- *; split. apply RestrictAddEq2; auto with stalmarck. apply RestrictAddEq1; auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)