proposition: Theorem eqStateRzTail : forall (a b : rZ) (S : State) (p : rZ * rZ), eqStateRz S a b -> eqStateRz (p :: S) a b.
proof: Proof. intros a b S p H'; elim H'; auto with stalmarck. intros a0 b0 S0 H'0. apply eqStateRzIn; simpl in |- *; auto with stalmarck. intros a0 b0 c S0 H'0 H'1 H'2 H'3. apply eqStateRzTrans with (b := b0); auto with stalmarck. intros a0 b0 c S0 H'0 H'1. apply eqStateRzContr with (a := a0); auto with stalmarck. Qed.
imports: Coq(List)