- change in H with (a⎻* ∘ A o1 = a'⎻* ∘ A o1);
- change in H1 with (b⎻* ∘ A o2 = b'⎻* ∘ A o2);
- apply (.= H‡#);
- intro x;
-
- change with (eq1 (oa_P (carrbt o3)) (b⎻* (a'⎻* (A o1 x))) (b'⎻*(a'⎻* (A o1 x))));
- lapply (saturated o1 o2 a' (A o1 x):?) as X;
- [ apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1) ]
- change in X with (eq1 (oa_P (carrbt o2)) (a'⎻* (A o1 x)) (A o2 (a'⎻* (A o1 x))));
- unfold uncurry_arrows;
- apply (.= †X); whd in H1;
- lapply (H1 (a'⎻* (A o1 x))) as X1;
- change in X1 with (eq1 (oa_P (carrbt o3)) (b⎻* (A o2 (a'⎻* (A o1 x)))) (b'⎻* (A o2 (a' \sup ⎻* (A o1 x)))));
- apply (.= X1);
- unfold uncurry_arrows;
- apply (†(X\sup -1));]
+ change in e with (a⎻* ∘ A o1 = a'⎻* ∘ A o1);
+ change in e1 with (b⎻* ∘ A o2 = b'⎻* ∘ A o2);
+ apply (.= e‡#);
+ intro x;
+ change with (eq1 ? (b⎻* (a'⎻* (A o1 x))) (b'⎻*(a'⎻* (A o1 x))));
+ apply (.= †(saturated o1 o2 a' (A o1 x) ?)); [
+ apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]
+ apply (.= (e1 (a'⎻* (A o1 x))));
+ change with (eq1 ? (b'⎻* (A o2 (a'⎻* (A o1 x)))) (b'⎻*(a'⎻* (A o1 x))));
+ apply (.= †(saturated o1 o2 a' (A o1 x):?)^-1); [
+ apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]
+ apply rule #;]