             make_poset_enrichment_coequalizer_cocone)
  ============================
   (φ₁ = φ₂)


Going to execute:
simple refine (p _)

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  ============================
   (φ₁ = φ₂)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  ============================
   (φ₁ = φ₂)


Going to execute:
simple refine (p _ _) ||
  simple refine (p _ _ _) ||
    simple refine (p _ _ _ _) ||
      simple refine (p _ _ _ _ _) ||
        simple refine (p _ _ _ _ _ _) ||
          simple refine (p _ _ _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
φ₁,
φ₂ : poset_sym_mon_closed_cat ⟦ P,
     E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
q : φ₁
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) =
    φ₂
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone)
The term "eq_monotone_function ?f" has type
 "∏ g0 : monotone_function ?R₁ ?R₂, (∏ x0 : ?X₁, ?f x0 = g0 x0) → ?f = g0"
while it is expected to have type "φ₁ = φ₂".
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
φ₁,
φ₂ : poset_sym_mon_closed_cat ⟦ P,
     E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
q : φ₁
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) =
    φ₂
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone)
The term "eq_monotone_function ?f" has type
 "∏ g0 : monotone_function ?R₁ ?R₂, (∏ x0 : ?X₁, ?f x0 = g0 x0) → ?f = g0"
while it is expected to have type "φ₁ = φ₂".

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  ============================
   (φ₁ = φ₂)


Going to execute:
simple refine (p _ _)

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  ============================
   (φ₁ = φ₂)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  ============================
   (φ₁ = φ₂)


Going to execute:
simple refine (p _ _ _) ||
  simple refine (p _ _ _ _) ||
    simple refine (p _ _ _ _ _) ||
      simple refine (p _ _ _ _ _ _) ||
        simple refine (p _ _ _ _ _ _ _) ||
          simple refine (p _ _ _ _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) || simple
                       refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
φ₁,
φ₂ : poset_sym_mon_closed_cat ⟦ P,
     E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
q : φ₁
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) =
    φ₂
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone)
The term "eq_monotone_function ?f ?g" has type
 "(∏ x0 : ?X₁, ?f x0 = ?g x0) → ?f = ?g" while it is expected to have type
 "φ₁ = φ₂".
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
φ₁,
φ₂ : poset_sym_mon_closed_cat ⟦ P,
     E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
q : φ₁
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) =
    φ₂
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone)
The term "eq_monotone_function ?f ?g" has type
 "(∏ x0 : ?X₁, ?f x0 = ?g x0) → ?f = ?g" while it is expected to have type
 "φ₁ = φ₂".

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  ============================
   (φ₁ = φ₂)


Going to execute:
simple refine (p _ _ _)

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  ============================
   (φ₁ = φ₂)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  ============================
   (∏ x0 : pr1 P, φ₁ x0 = φ₂ x0)


Going to execute:
intro z

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  ============================
   (∏ x0 : pr1 P, φ₁ x0 = φ₂ x0)


Going to execute:
<coq-core.plugins.ltac::intro@1> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
use poset_enrichment_coequalizer_arr_eq

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
simple_rapply p

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
fun p =>
  simple refine p ||
    simple refine (p _) ||
      simple refine (p _ _) ||
...                              simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _)
                               || simple refine
                               (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)

TcDebug (1) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
simple refine p ||
  simple refine (p _) ||
    simple refine (p _ _) ||
      simple refine (p _ _ _) ||
        simple refine (p _ _ _ _) ||
          simple refine (p _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                            simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                              simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)

TcDebug (1) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
simple refine p
Level 1: evaluation returns
simple refine p ||
  simple refine (p _) ||
    simple refine (p _ _) ||
      simple refine (p _ _ _) ||
        simple refine (p _ _ _ _) ||
          simple refine (p _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                            simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                              simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
where
p := poset_enrichment_coequalizer_arr_eq
of type
uconstr of type tacvalue


TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
simple refine (p _) ||
  simple refine (p _ _) ||
    simple refine (p _ _ _) ||
      simple refine (p _ _ _ _) ||
        simple refine (p _ _ _ _ _) ||
          simple refine (p _ _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                            simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
φ₁,
φ₂ : poset_sym_mon_closed_cat ⟦ P,
     E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
q : φ₁
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) =
    φ₂
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone)
z : pr1 P
The term "poset_enrichment_coequalizer_arr_eq" has type
 "∏ (EEC : poset_enrichment_coequalizers) (x y z : C) 
  (f g : C ⟦ x, y ⟧)
  (h₁ h₂ : C ⟦ poset_enrichment_obj_coequalizer EEC f g, z ⟧),
  poset_enrichment_obj_coeq_in EEC f g · h₁ =
  poset_enrichment_obj_coeq_in EEC f g · h₂ → h₁ = h₂"
while it is expected to have type "φ₁ z = φ₂ z".
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
φ₁,
φ₂ : poset_sym_mon_closed_cat ⟦ P,
     E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
q : φ₁
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) =
    φ₂
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone)
z : pr1 P
The term "poset_enrichment_coequalizer_arr_eq" has type
 "∏ (EEC : poset_enrichment_coequalizers) (x y z : C) 
  (f g : C ⟦ x, y ⟧)
  (h₁ h₂ : C ⟦ poset_enrichment_obj_coequalizer EEC f g, z ⟧),
  poset_enrichment_obj_coeq_in EEC f g · h₁ =
  poset_enrichment_obj_coeq_in EEC f g · h₂ → h₁ = h₂"
while it is expected to have type "φ₁ z = φ₂ z".

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
simple refine (p _)

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
<coq-core.plugins.ltac::simple_refine@0> $1

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  q : φ₁
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone) =
      φ₂
      · precomp_arr E' w
          (enriched_coequalizer_cocone_in E' f g
             make_poset_enrichment_coequalizer_cocone)
  z : pr1hSet
        ?X451@{__:=?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0; __:=?M0; __:=?M0; __:=?M0; __:=
               ?M0}
  ============================
   (φ₁ z = φ₂ z)


Going to execute:
simple refine (p _ _) ||
  simple refine (p _ _ _) ||
    simple refine (p _ _ _ _) ||
      simple refine (p _ _ _ _ _) ||
        simple refine (p _ _ _ _ _ _) ||
          simple refine (p _ _ _ _ _ _ _) ||
            simple refine (p _ _ _ _ _ _ _ _) ||
              simple refine (p _ _ _ _ _ _ _ _ _) ||
                simple refine (p _ _ _ _ _ _ _ _ _ _) ||
                  simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
                    simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
                      simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                        simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
                          simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
φ₁,
φ₂ : poset_sym_mon_closed_cat ⟦ P,
     E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
q : φ₁
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) =
    φ₂
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone)
z : pr1 P
The term "@poset_enrichment_coequalizer_arr_eq ?EEC" has type
 "∏ (x0 y0 z0 : C) (f0 g0 : C ⟦ x0, y0 ⟧)
  (h₁ h₂ : C ⟦ poset_enrichment_obj_coequalizer ?EEC f0 g0, z0 ⟧),
  poset_enrichment_obj_coeq_in ?EEC f0 g0 · h₁ =
  poset_enrichment_obj_coeq_in ?EEC f0 g0 · h₂ → h₁ = h₂"
while it is expected to have type "φ₁ z = φ₂ z".
Level 0: In environment
C : category
E : poset_enrichment C
E' := make_enrichment_over_poset C E : enrichment C poset_sym_mon_closed_cat
EEC : poset_enrichment_coequalizers
x, y : C
f, g : C ⟦ x, y ⟧
w : C
P : poset_sym_mon_closed_cat
φ₁,
φ₂ : poset_sym_mon_closed_cat ⟦ P,
     E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
q : φ₁
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone) =
    φ₂
    · precomp_arr E' w
        (enriched_coequalizer_cocone_in E' f g
           make_poset_enrichment_coequalizer_cocone)
z : pr1 P
The term "@poset_enrichment_coequalizer_arr_eq ?EEC" has type
 "∏ (x0 y0 z0 : C) (f0 g0 : C ⟦ x0, y0 ⟧)
  (h₁ h₂ : C ⟦ poset_enrichment_obj_coequalizer ?EEC f0 g0, z0 ⟧),
  poset_enrichment_obj_coeq_in ?EEC f0 g0 · h₁ =
  poset_enrichment_obj_coeq_in ?EEC f0 g0 · h₂ → h₁ = h₂"
while it is expected to have type "φ₁ z = φ₂ z".

TcDebug (0) > 
Goal:
  
  C : category
  E : poset_enrichment C
  E' := make_enrichment_over_poset C E
     : enrichment C poset_sym_mon_closed_cat
  EEC : poset_enrichment_coequalizers
  x : ob C
  y : ob C
  f : C ⟦ x, y ⟧
  g : C ⟦ x, y ⟧
  w : ob C
  P : ob poset_sym_mon_closed_cat
  φ₁ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
  φ₂ : poset_sym_mon_closed_cat ⟦ P,
       E' ⦃ make_poset_enrichment_coequalizer_cocone, w ⦄ ⟧
