proposition: Theorem eqConstrStateIn : forall (a b : rZ) (S : State), In (a, b) S -> eqConstrState S a b.
proof: Proof. intros a b L; elim L; simpl in |- *; auto with stalmarck. intros H'; elim H'; auto with stalmarck. intros a0 l H' H'0; Elimc H'0; intros H'0; [ rewrite H'0 | idtac ]; auto with stalmarck. Qed.
imports: Coq(List)