simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
[ apply (. (e^-1‡#)); | apply (. (e‡#)); ]
apply x;
simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
[ apply (. (e^-1‡#)); | apply (. (e‡#)); ]
apply x;