| intros; split; intros; cases e2; exists [1,3: apply w]
[ apply (. (#‡e1^-1)‡(e^-1‡#)); assumption
| apply (. (#‡e1)‡(e‡#)); assumption]]
qed.
| intros; split; intros; cases e2; exists [1,3: apply w]
[ apply (. (#‡e1^-1)‡(e^-1‡#)); assumption
| apply (. (#‡e1)‡(e‡#)); assumption]]
qed.