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;
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;