let EH_x_y := (rlucancel_inv (ulnat_x0 [-] urnat_y0))^ @ wlrnat_x_y @ rlucancel_inv (urnat_y1 [-] ulnat_x1) in let EH_y_x := (rlucancel_inv (ulnat_y1 [-] urnat_x1))^ @ wlrnat_y_x @ rlucancel_inv (urnat_x0 [-] ulnat_y0) in EH_x_y @ EH_y_x = 1. Proof. pose (H_whiskerR_wlrnat_x_y := moveL_Mp _ _ _ (moveL_pV _ _ _ (whiskerR_p1 wlrnat_x_y))). apply moveL_pV in wlrnat_V_x_y. apply (concat H_whiskerR_wlrnat_x_y^) in wlrnat_V_x_y. apply moveL_Vp, moveL_pV in wlrnat_V_x_y. apply symmetry in wlrnat_V_x_y. destruct wlrnat_V_x_y. clear wlrnat_V_x_y. clear H_whiskerR_wlrnat_x_y. revert ulnat_x0 ehlnat_1p_x0. snrapply equiv_path_ind_rlucancel. revert ulnat_x1 ehlnat_1p_x1. snrapply equiv_path_ind_rlucancel. revert urnat_y0 ehrnat_p1_y0. snrapply equiv_path_ind_rlucancel. revert urnat_y1 ehrnat_p1_y1. snrapply equiv_path_ind_rlucancel. revert x0 urnat_x0. snrapply equiv_path_ind_rlucancel. revert x1 urnat_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 wlrnat_y_x. revert wrx0 ehlnat_x0. snrapply equiv_path_ind_rlucancel. revert wrx1 ehlnat_x1. snrapply equiv_path_ind_rlucancel. revert wly0 ehrnat_y0. snrapply equiv_path_ind_rlucancel. revert wly1 ehrnat_y1. snrapply equiv_path_ind_rlucancel. destruct wry0, wry1, wlx1. clear wry0 wry1 wlx1. revert wlx0. snrapply equiv_path_ind_lrucancel. reflexivity. Defined.
From HoTT Require Import Basics Types.