+ 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);]]