{X : Type} {a b c d e f : X} {wlx0 x0 wrx0 : a = b} {wlx1 x1 wrx1 : c = d} {wlx2 x2 wrx2 : e = f} {wly0 y0 wry0 : b = d} {wly1 y1 wry1 : a = c} {wlz0 z0 wrz0 : d = f} {wlz1 z1 wrz1 : c = e} {wlyz0 wryz0 : b = f} {wlyz1 wryz1 : a = e} {ulnat_x0 : wlx0 @ 1 = 1 @ x0} {urnat_x0 : wrx0 @ 1 = 1 @ x0} {ulnat_x1 : wlx1 @ 1 = 1 @ x1} {urnat_x1 : wrx1 @ 1 = 1 @ x1} {ulnat_x2 : wlx2 @ 1 = 1 @ x2} {urnat_x2 : wrx2 @ 1 = 1 @ x2} {ulnat_y0 : wly0 @ 1 = 1 @ y0} {urnat_y0 : wry0 @ 1 = 1 @ y0} {ulnat_y1 : wly1 @ 1 = 1 @ y1} {urnat_y1 : wry1 @ 1 = 1 @ y1} {ulnat_z0 : wlz0 @ 1 = 1 @ z0} {urnat_z0 : wrz0 @ 1 = 1 @ z0} {ulnat_z1 : wlz1 @ 1 = 1 @ z1} {urnat_z1 : wrz1 @ 1 = 1 @ z1} {ulnat_yz0 : wlyz0 @ 1 = 1 @ (y0 @ z0)} {urnat_yz0 : wryz0 @ 1 = 1 @ (y0 @ z0)} {ulnat_yz1 : wlyz1 @ 1 = 1 @ (y1 @ z1)} {urnat_yz1 : wryz1 @ 1 = 1 @ (y1 @ z1)} {ehlnat_x0 : wlx0 @ 1 = 1 @ wrx0} {ehlnat_x1 : wlx1 @ 1 = 1 @ wrx1} {ehlnat_x2 : wlx2 @ 1 = 1 @ wrx2} {ehrnat_y0 : wry0 @ 1 = 1 @ wly0} {ehrnat_y1 : wry1 @ 1 = 1 @ wly1} {ehrnat_z0 : wrz0 @ 1 = 1 @ wlz0} {ehrnat_z1 : wrz1 @ 1 = 1 @ wlz1} {ehrnat_yz0 : wryz0 @ 1 = 1 @ wlyz0} {ehrnat_yz1 : wryz1 @ 1 = 1 @ wlyz1} {wlrnat_x_y : wlx0 @ wry0 = wry1 @ wlx1} {wlrnat_y_x : wly1 @ wrx1 = wrx0 @ wly0} {wlrnat_x_z : wlx1 @ wrz0 = wrz1 @ wlx2} {wlrnat_z_x : wlz1 @ wrx2 = wrx1 @ wlz0} {wlrnat_x_yz : wlx0 @ wryz0 = wryz1 @ wlx2} {wlrnat_yz_x : wlyz1 @ wrx2 = wrx0 @ wlyz0} {wrpp_yz0 : wry0 @ wrz0 = wryz0} {wlpp_yz0 : wly0 @ wlz0 = wlyz0} {wrpp_yz1 : wry1 @ wrz1 = wryz1} {wlpp_yz1 : wly1 @ wlz1 = wlyz1} {H_ulnat_yz0 : (ulnat_y0 [-] ulnat_z0) = whiskerR wlpp_yz0 _ @ ulnat_yz0} {H_urnat_yz0 : (urnat_y0 [-] urnat_z0) = whiskerR wrpp_yz0 _ @ urnat_yz0} {H_ulnat_yz1 : (ulnat_y1 [-] ulnat_z1) = whiskerR wlpp_yz1 _ @ ulnat_yz1} {H_urnat_yz1 : (urnat_y1 [-] urnat_z1) = whiskerR wrpp_yz1 _ @ urnat_yz1} {H_ehrnat_yz0 : (ehrnat_y0 [-] ehrnat_z0) @ whiskerL _ wlpp_yz0 = whiskerR wrpp_yz0 _ @ ehrnat_yz0} {H_ehrnat_yz1 : (ehrnat_y1 [-] ehrnat_z1) @ whiskerL _ wlpp_yz1 = whiskerR wrpp_yz1 _ @ ehrnat_yz1} {H_wlrnat_x_yz : (wlrnat_x_y [I] wlrnat_x_z) @ whiskerR wrpp_yz1 _ = whiskerL _ wrpp_yz0 @ wlrnat_x_yz} {H_wlrnat_yz_x : (wlrnat_y_x [-] wlrnat_z_x) @ whiskerL _ wlpp_yz0 = whiskerR wlpp_yz1 _ @ wlrnat_yz_x} (ehlnat_1p_x0 : (ehlnat_x0 [I] urnat_x0) @ 1 = 1 @ ulnat_x0) (ehlnat_1p_x1 : (ehlnat_x1 [I] urnat_x1) @ 1 = 1 @ ulnat_x1) (ehlnat_1p_x2 : (ehlnat_x2 [I] urnat_x2) @ 1 = 1 @ ulnat_x2) {ehrnat_p1_y0 : (ehrnat_y0 [I] ulnat_y0) @ 1 = 1 @ urnat_y0} {ehrnat_p1_y1 : (ehrnat_y1 [I] ulnat_y1) @ 1 = 1 @ urnat_y1} {ehrnat_p1_z0 : (ehrnat_z0 [I] ulnat_z0) @ 1 = 1 @ urnat_z0} {ehrnat_p1_z1 : (ehrnat_z1 [I] ulnat_z1) @ 1 = 1 @ urnat_z1} {ehrnat_p1_yz0 : (ehrnat_yz0 [I] ulnat_yz0) @ 1 = 1 @ urnat_yz0} {ehrnat_p1_yz1 : (ehrnat_yz1 [I] ulnat_yz1) @ 1 = 1 @ urnat_yz1} {wlrnat_V_x_y : whiskerR wlrnat_x_y _ @ (ehrnat_y1 [-] ehlnat_x1) = (ehlnat_x0 [-] ehrnat_y0) @ whiskerL _ wlrnat_y_x^} {wlrnat_V_x_z : whiskerR wlrnat_x_z _ @ (ehrnat_z1 [-] ehlnat_x2) = (ehlnat_x1 [-] ehrnat_z0) @ whiskerL _ wlrnat_z_x^} {wlrnat_V_x_yz : whiskerR wlrnat_x_yz _ @ (ehrnat_yz1 [-] ehlnat_x2) = (ehlnat_x0 [-] ehrnat_yz0) @ whiskerL _ wlrnat_yz_x^} (H_ehrnat_p1_yz0 : Ehrnat_p1_pp 1 1 H_ehrnat_yz0 H_ulnat_yz0 H_urnat_yz0 ehrnat_p1_y0 ehrnat_p1_z0 = ehrnat_p1_yz0) (H_ehrnat_p1_yz1 : Ehrnat_p1_pp 1 1 H_ehrnat_yz1 H_ulnat_yz1 H_urnat_yz1 ehrnat_p1_y1 ehrnat_p1_z1 = ehrnat_p1_yz1) (H_wlrnat_V_x_yz : Wlrnat_V_p_pp H_ehrnat_yz0 H_ehrnat_yz1 H_wlrnat_x_yz H_wlrnat_yz_x wlrnat_V_x_y wlrnat_V_x_z = wlrnat_V_x_yz) : let eh_x_y := concat_p_pp x0 y0 z0 @ whiskerR (((rlucancel_inv (ulnat_x0 [-] urnat_y0))^ @ wlrnat_x_y) @ rlucancel_inv (urnat_y1 [-] ulnat_x1)) z0 in whiskerR (concat_p1 _ @@ concat_p1 _) eh_x_y @ whiskerR (eh_V_gen (ehlnat_1p_x0) (ehlnat_1p_x2) (ehrnat_p1_yz0) (ehrnat_p1_yz1) wlrnat_V_x_yz) eh_x_y @ lrucancel 1 @ whiskerL eh_x_y (Syllepsis.concat_pp_p_p_pp _ _ _)^ @ whiskerL eh_x_y (concat_p1 _ @@ concat_p1 _)^ = (eh_p_pp_gen H_urnat_yz0 H_urnat_yz1 H_wlrnat_x_yz [-] lrucancel (whiskerL _ (ap (fun p => whiskerL y1 p) (moveL_V1 _ _ (eh_V_gen ehlnat_1p_x1 ehlnat_1p_x2 ehrnat_p1_z0 ehrnat_p1_z1 wlrnat_V_x_z))))) [-] (eh_pp_p_gen H_ulnat_yz1 H_ulnat_yz0 H_wlrnat_yz_x [-] lrucancel (whiskerL _ (ap (fun p => whiskerR p z0) (moveL_1V _ _ (eh_V_gen ehlnat_1p_x0 ehlnat_1p_x1 ehrnat_p1_y0 ehrnat_p1_y1 wlrnat_V_x_y))))). Proof. destruct H_ehrnat_p1_yz0, H_ehrnat_p1_yz1, H_wlrnat_V_x_yz. revert_until a. generalize_goal lem. { intros P H; intros. destruct wry0, wry1, wrz0, wrz1. destruct wrpp_yz0, wlpp_yz0, wrpp_yz1, wlpp_yz1. revert wlrnat_x_yz H_wlrnat_x_yz. snrapply equiv_path_ind_moveL_Mp. revert wlrnat_x_y wlrnat_V_x_y. snrapply (equiv_path_ind (equiv_helper _ _)). revert wlrnat_x_z wlrnat_V_x_z. snrapply (equiv_path_ind (equiv_helper _ _)). revert ulnat_x0 ehlnat_1p_x0. snrapply equiv_path_ind_rlucancel. revert ulnat_x1 ehlnat_1p_x1. snrapply equiv_path_ind_rlucancel. revert ulnat_x2 ehlnat_1p_x2. snrapply equiv_path_ind_rlucancel. revert urnat_yz0 H_urnat_yz0. snrapply equiv_path_ind_moveL_Mp. revert urnat_yz1 H_urnat_yz1. snrapply equiv_path_ind_moveL_Mp. revert wlrnat_yz_x H_wlrnat_yz_x. snrapply equiv_path_ind_moveL_Mp. revert ehrnat_yz0 H_ehrnat_yz0. snrapply equiv_path_ind_moveL_Mp. revert ehrnat_yz1 H_ehrnat_yz1. snrapply equiv_path_ind_moveL_Mp. revert ulnat_yz1 H_ulnat_yz1. snrapply equiv_path_ind_moveL_Mp. revert ulnat_yz0 H_ulnat_yz0. snrapply equiv_path_ind_moveL_Mp. revert urnat_y0 ehrnat_p1_y0. snrapply equiv_path_ind_rlucancel. revert urnat_y1 ehrnat_p1_y1. snrapply equiv_path_ind_rlucancel. revert urnat_z0 ehrnat_p1_z0. snrapply equiv_path_ind_rlucancel. revert urnat_z1 ehrnat_p1_z1. snrapply equiv_path_ind_rlucancel. revert x0 urnat_x0. snrapply equiv_path_ind_rlucancel. revert x1 urnat_x1. snrapply equiv_path_ind_rlucancel. revert x2 urnat_x2. 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 ulnat_z0. snrapply equiv_path_ind_rlucancel. revert z1 ulnat_z1. snrapply equiv_path_ind_rlucancel. revert wlrnat_y_x. revert wrx0 ehlnat_x0. snrapply equiv_path_ind_rlucancel. revert wlrnat_z_x. revert wrx1 ehlnat_x1. snrapply equiv_path_ind_rlucancel. revert wrx2 ehlnat_x2. snrapply equiv_path_ind_rlucancel. revert wly0 ehrnat_y0. snrapply equiv_path_ind_rlucancel. revert wly1 ehrnat_y1. snrapply equiv_path_ind_rlucancel. revert wlz0 ehrnat_z0. snrapply equiv_path_ind_rlucancel. revert wlz1 ehrnat_z1. snrapply equiv_path_ind_rlucancel. revert wlx1. snrapply equiv_path_ind_lrucancel. revert wlx0. snrapply equiv_path_ind_lrucancel. destruct wlx2. exact H. } apply lem. reflexivity. Qed.
From HoTT Require Import Basics Types.