proposition: Theorem stripRzDecProp2 : forall (S1 S2 : State) (a b : rZ), In (a, b) (stripRzDec S1 S2) -> eqConstrState S1 a b.
proof: Proof. intros S1 S2; elim S2; simpl in |- *; auto with stalmarck. intros a b H'; Elimc H'; clear a b. intros p; case p; auto with stalmarck. intros c d l H' a b; case (eqConstrStateDec S1 c d); simpl in |- *; auto with stalmarck. intros H'0 H'1; Elimc H'1; intros H'1; [ generalize H'0; inversion H'1 | idtac ]; auto with stalmarck. Qed.
imports: Coq(List)