let EH_x_z := (rlucancel_inv (ulnat_x0 [-] urnat_z1))^ @ wlrnat_x_z @ rlucancel_inv (urnat_z2 [-] ulnat_x1) in let EH_y_z := (rlucancel_inv (ulnat_y0 [-] urnat_z0))^ @ wlrnat_y_z @ rlucancel_inv (urnat_z1 [-] ulnat_y1) in let EH_xy_z := (rlucancel_inv (ulnat_xy0 [-] urnat_z0))^ @ wlrnat_xy_z @ rlucancel_inv (urnat_z2 [-] ulnat_xy1) in EH_xy_z @ (concat_p_pp _ _ _ @ whiskerR EH_x_z^ _) = concat_pp_p _ _ _ @ whiskerL _ EH_y_z @ concat_p_pp _ _ _. Proof. apply moveR_Vp in H_ulnat_xy0, H_ulnat_xy1, H_wlrnat_xy_z. destruct H_ulnat_xy0, H_ulnat_xy1, H_wlrnat_xy_z. clear H_ulnat_xy0 H_ulnat_xy1 H_wlrnat_xy_z. destruct wlpp_xy0, wlpp_xy1. clear wlpp_xy0 wlpp_xy1. revert x0 ulnat_x0. snrapply equiv_path_ind_rlucancel. revert x1 ulnat_x1. snrapply equiv_path_ind_rlucancel. revert y0 ulnat_y0. snrapply equiv_path_ind_rlucancel. revert y1 ulnat_y1. snrapply equiv_path_ind_rlucancel. revert z0 urnat_z0. snrapply equiv_path_ind_rlucancel. revert z1 urnat_z1. snrapply equiv_path_ind_rlucancel. revert z2 urnat_z2. snrapply equiv_path_ind_rlucancel. destruct wlx0, wlx1, wly0, wly1. clear wlx0 wlx1 wly0 wly1. revert wrz2 wlrnat_x_z. snrapply equiv_path_ind_lrucancel. revert wrz1 wlrnat_y_z. snrapply equiv_path_ind_lrucancel. destruct wrz0. clear wrz0. reflexivity. Defined.
From HoTT Require Import Basics Types.