apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
apply (.= (e1 (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))));