proposition: Theorem inclStateAddEqInv : forall (p q : rZ) (S1 S2 : State), inclState S1 S2 -> eqStateRz S2 p q -> inclState (addEq (p, q) S1) S2.
proof: Proof. intros p0 q0 S1 S2 H' H'0; red in |- *; auto with stalmarck. intros i j H'1; generalize H'0 H'; auto with stalmarck. cut (exists S3 : State, S3 = addEq (p0, q0) S1); auto with stalmarck. intros H'2; Elimc H'2; intros S3 E; rewrite <- E in H'1; auto with stalmarck. generalize E; elim H'1; auto with stalmarck. intros a b L H'2 H'3; rewrite H'3 in H'2; simpl in H'2; case H'2; auto with stalmarck. intros H'4; inversion H'4; auto with stalmarck. intros a b S H'2 H'3 H'4 H'5 H'6; auto with stalmarck. apply eqStateRzSym; auto with stalmarck. intros a b c S H'2 H'3 H'4 H'5 H'6 H'7 H'8. apply eqStateRzTrans with (b := b); auto with stalmarck. intros a b c S H'2 H'3 H'4 H'5 H'6. apply eqStateRzContr with (a := a); auto with stalmarck. exists (addEq (p0, q0) S1); auto with stalmarck. Qed.
imports: Coq(List)