- intro x;
- change with (b⎻* (a'⎻* (A o1 x)) = b'⎻*(a'⎻* (A o1 x)));
- alias symbol "trans" = "trans1".
- alias symbol "prop1" = "prop11".
- alias symbol "invert" = "setoid1 symmetry".
- lapply (.= †(saturated o1 o2 a' (A o1 x) : ?));
- [3: apply (b⎻* ); | 5: apply Hletin; |1,2: skip;
- |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".
- lapply (†((saturated ?? a' (A o1 x) : ?) ^ -1));
- [2: apply (b'⎻* ); |4: apply Hletin; | skip;
- |apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-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 #;]