apply rule (#‡ASSOC1\sup -1);
| intros; simplify;
change with ((a⎻* ∘ (id1 ? o1)⎻* ) ∘ A o1 = a⎻* ∘ A o1);
- apply rule (†((id_neutral_right1 ????)‡#));
- apply refl1*)
- | intros; simplify; intro; simplify;
- apply (.= †((id_neutral_left1 ????)‡#));
- apply refl1]
+ apply (#‡(id_neutral_right1 : ?));
+ | intros; simplify;
+ change with (((id1 ? o2)⎻* ∘ a⎻* ) ∘ A o1 = a⎻* ∘ A o1);
+ apply (#‡(id_neutral_left1 : ?));]
qed.
(*