proposition: Theorem eqStateEq2 : forall (S : State) (q r s t u v w x : rZ), eqStateRz S q s -> eqStateRz S r t -> eqStateRz S u w -> eqStateRz S v x -> eqState (addEq (q, r) (addEq (u, v) S)) (addEq (s, t) (addEq (w, x) S)).
proof: Proof. intros S q r s t u v w x Eq1 Eq2 Eq3 Eq4; 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. 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 := w); auto with stalmarck. apply eqStateRzTrans with (b := x); 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; auto with stalmarck. rewrite <- H0; rewrite <- H1. apply eqStateRzTrans with (b := q); auto with stalmarck. 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 := u); auto with stalmarck. Qed.
imports: Stalmarck(interState doTriplet)