proposition: Theorem eqStateRzPImpeqConstrState : forall (S : State) (a b : rZ), eqStateRz S a b -> eqConstrState S a b.
proof: Proof. intros S a b H'; elim H'; auto with stalmarck. intros a0 b0 c S0 H'0 H'1 H'2 H'3. apply eqConstrStateTrans with (b := b0); auto with stalmarck. intros a0 b0 c S0 H'0 H'1. apply eqConstrStateContrGen with (a := a0); auto with stalmarck. Qed.
imports: Coq(List)