(ehrnat_yz [I] ulnat_yz) @ whiskerR H_a02 _ = whiskerL _ H_c02 @ urnat_yz. Proof. apply moveR_Vp in H_urnat_yz, H_ulnat_yz, H_ehrnat_yz. destruct H_urnat_yz, H_ulnat_yz, H_ehrnat_yz. clear H_urnat_yz H_ulnat_yz H_ehrnat_yz. apply moveR_Vp in ehrnat_p1_y, ehrnat_p1_z. destruct ehrnat_p1_y, ehrnat_p1_z. clear ehrnat_p1_y ehrnat_p1_z. destruct H_a02, H_c02. clear H_a02 H_c02. destruct wrpp_yz, wlpp_yz. clear wrpp_yz wlpp_yz. destruct a01, a12, b01, b12, c01, c12. clear a01 a12 b01 b12 c01 c12. revert y ulnat_y. snrapply equiv_path_ind_rlucancel. revert z ulnat_z. snrapply equiv_path_ind_rlucancel. revert wly ehrnat_y. snrapply equiv_path_ind_rlucancel. revert wlz ehrnat_z. snrapply equiv_path_ind_rlucancel. destruct wry, wrz. clear wry wrz. reflexivity. Defined.
From HoTT Require Import Basics Types.