- intro x;
- change with (eq1 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 ? (a'⎻* (A o1 x)) (A o2 (a'⎻* (A o1 x))));
- alias symbol "trans" = "trans1".
- alias symbol "prop1" = "prop11".
- apply (.= †X);
- whd in e1;
- lapply (e1 (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);
- alias symbol "invert" = "setoid1 symmetry".
- apply (†(X\sup -1));]
+ intro x;
+ change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x))));
+ apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
+ apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
+ apply (.= (e1 (a'⎻* (oA o1 x))));
+ change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x))));
+ apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [
+ apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
+ apply rule #;]