let EH_x_y := (rlucancel_inv (ulnat_x0 [-] urnat_y0))^ @ wlrnat_x_y @ rlucancel_inv (urnat_y1 [-] ulnat_x1) in let EH_x_z := (rlucancel_inv (ulnat_x1 [-] urnat_z0))^ @ wlrnat_x_z @ rlucancel_inv (urnat_z1 [-] ulnat_x2) in let EH_x_yz := (rlucancel_inv (ulnat_x0 [-] urnat_yz0))^ @ wlrnat_x_yz @ rlucancel_inv (urnat_yz1 [-] ulnat_x2) in EH_x_yz @ (concat_pp_p _ _ _ @ whiskerL _ EH_x_z^) = concat_p_pp _ _ _ @ whiskerR EH_x_y _ @ concat_pp_p _ _ _. Proof. apply moveR_Vp in H_urnat_yz0, H_urnat_yz1, H_wlrnat_x_yz. destruct H_urnat_yz0, H_urnat_yz1, H_wlrnat_x_yz. clear H_urnat_yz0 H_urnat_yz1 H_wlrnat_x_yz. destruct wrpp_yz0, wrpp_yz1. clear wrpp_yz0 wrpp_yz1. revert x0 ulnat_x0. snrapply equiv_path_ind_rlucancel. revert x1 ulnat_x1. snrapply equiv_path_ind_rlucancel. revert x2 ulnat_x2. snrapply equiv_path_ind_rlucancel. revert y0 urnat_y0. snrapply equiv_path_ind_rlucancel. revert y1 urnat_y1. snrapply equiv_path_ind_rlucancel. revert z0 urnat_z0. snrapply equiv_path_ind_rlucancel. revert z1 urnat_z1. snrapply equiv_path_ind_rlucancel. destruct wry0, wry1, wrz0, wrz1. clear wry0 wry1 wrz0 wrz1. revert wlx2 wlrnat_x_z. snrapply equiv_path_ind_rlucancel. revert wlx1 wlrnat_x_y. snrapply equiv_path_ind_rlucancel. destruct wlx0. clear wlx0. reflexivity. Defined.
From HoTT Require Import Basics Types.