(* case 3: zeta, delta (repeated) *)
| @ex2_commute /3 width=10 by tpr_conf_delta_zeta/
(* case 4: delta, zeta *)
| /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
(* case 5: zeta, zeta *)
(* case 3: zeta, delta (repeated) *)
| @ex2_commute /3 width=10 by tpr_conf_delta_zeta/
(* case 4: delta, zeta *)
| /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
(* case 5: zeta, zeta *)