- intro x;
- change with (b⎻* (a'⎻* (A o1 x)) = b'⎻*(a'⎻* (A o1 x)));
- alias symbol "trans" = "trans1".
- alias symbol "prop1" = "prop11".
- apply (.= †(saturated o1 o2 a' (A o1 x) : ?));
- [ apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1); ]
- change in e1 with (∀x.b⎻* (A o2 x) = b'⎻* (A o2 x));
- apply (.= (e1 (a'⎻* (A o1 x))));
- alias symbol "invert" = "setoid1 symmetry".
- apply (†((saturated ?? a' (A o1 x) : ?) ^ -1));
- apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1);]
+ intro x;
+ change with (b⎻* (a'⎻* (oA o1 x)) =_1 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 (b'⎻* (oA o2 (a'⎻* (oA o1 x))) =_1 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 #;]