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