- apply (.= †(saturated o1 o2 a' (A o1 x) : ?));
- [ apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1); ]
+ 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); ]