proposition: Theorem eqStateEq1 : forall (S : State) (q r s t : rZ), eqStateRz S q s -> eqStateRz S r t -> eqState (addEq (q, r) S) (addEq (s, t) S).
proof: Proof. intros S q r s t Eq1 Eq2; split. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a b H'0; Elimc H'0; intros H'0; auto with stalmarck. inversion H'0; clear H'0; auto with stalmarck. rewrite <- H0; rewrite <- H1. apply eqStateRzTrans with (b := s); auto with stalmarck. apply eqStateRzTrans with (b := t); auto with stalmarck. apply inclStateIn; simpl in |- *; auto with stalmarck. intros a b H'0; Elimc H'0; intros H'0; auto with stalmarck. inversion H'0; clear H'0. rewrite <- H0; rewrite <- H1. apply eqStateRzTrans with (b := q); auto with stalmarck. Qed.
imports: Stalmarck(interState doTriplet)