graph_unsucc_equiv_edge@{} (x y : vert A) : iff@{s s s} (edge A x y) (edge B (graph_unsucc_equiv_vert x) (graph_unsucc_equiv_vert y)). Proof. pose (h := e (inl x) (inl y)). rewrite <- (unfunctor_sum_l_beta f Ha x) in h. rewrite <- (unfunctor_sum_l_beta f Ha y) in h. exact h. Qed.
Require Import Basics. Require Import Types. Require Import HProp. Require Import Universes.Smallness.