whiskerR wlrnat_x_yz _ @ (ehrnat_yz1 [-] ehlnat_x2) = (ehlnat_x0 [-] ehrnat_yz0) @ whiskerL _ wlrnat_yz_x^. Proof. apply moveR_Vp in H_ehrnat_yz0, H_ehrnat_yz1. destruct H_ehrnat_yz0, H_ehrnat_yz1. clear H_ehrnat_yz0 H_ehrnat_yz1. apply moveR_Vp in H_wlrnat_x_yz, H_wlrnat_yz_x. destruct H_wlrnat_x_yz, H_wlrnat_yz_x. clear H_wlrnat_x_yz H_wlrnat_yz_x. destruct a01, b01, c01, d01, e01, f01. clear a01 b01 c01 d01 e01 f01. pose (H_whiskerR_wlrnat_x_y := moveL_Mp _ _ _ (moveL_pV _ _ _ (whiskerR_p1 wlrnat_x_y))). pose (H_whiskerR_wlrnat_x_z := moveL_Mp _ _ _ (moveL_pV _ _ _ (whiskerR_p1 wlrnat_x_z))). 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. apply moveL_pV in wlrnat_V_x_z. apply (concat H_whiskerR_wlrnat_x_z^) in wlrnat_V_x_z. apply moveL_Vp, moveL_pV in wlrnat_V_x_z. apply symmetry in wlrnat_V_x_z. destruct wlrnat_V_x_z. clear wlrnat_V_x_z. clear H_whiskerR_wlrnat_x_y H_whiskerR_wlrnat_x_z. destruct wrpp_yz0, wlpp_yz0, wrpp_yz1, wlpp_yz1. clear wrpp_yz0 wlpp_yz0 wrpp_yz1 wlpp_yz1. revert wlrnat_y_x wlrnat_z_x. revert wrx0 ehlnat_x0. snrapply equiv_path_ind_rlucancel. 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. destruct wry0, wry1, wrz0, wrz1. clear wry0 wry1 wrz0 wrz1. revert wlx0. snrapply equiv_path_ind_lrucancel. revert wlx1. snrapply equiv_path_ind_lrucancel. destruct wlx2. clear wlx2. reflexivity. Defined.
From HoTT Require Import Basics Types.