cases g
case mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
f : Morphism G₁ G₂
toFuncV✝ : V₃ → V✝
toFuncE✝ : E₃ → E✝
toFuncV_init✝ : ∀ (e : E₃), toFuncV✝ (G₃.ι e) = G₄.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₃), toFuncE✝ (G₃.bar e) = G₄.bar (toFuncE✝ e)
⊢ comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
      (comp g f) =
    comp
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } g)
      f
case mk.mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
f : Morphism G₁ G₂
toFuncV✝¹ : V₃ → V✝
toFuncE✝¹ : E₃ → E✝
toFuncV_init✝¹ : ∀ (e : E₃), toFuncV✝¹ (G₃.ι e) = G₄.ι (toFuncE✝¹ e)
toFuncE_bar✝¹ : ∀ (e : E₃), toFuncE✝¹ (G₃.bar e) = G₄.bar (toFuncE✝¹ e)
toFuncV✝ : V₂ → V₃
toFuncE✝ : E₂ → E₃
toFuncV_init✝ : ∀ (e : E₂), toFuncV✝ (G₂.ι e) = G₃.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₂), toFuncE✝ (G₂.bar e) = G₃.bar (toFuncE✝ e)
⊢ comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
        f) =
    comp
      (comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
        { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ })
      f