Proofgold Address

Definition 43cf7.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x0 x4 x5 ⟶ x3 x4 x5) ⟶ (∀ x4 . x3 x4 x4) ⟶ (∀ x4 x5 . x3 x4 x5 ⟶ x3 x5 x4) ⟶ (∀ x4 x5 x6 . x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6) ⟶ x3 x1 x2
Theorem f187c.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x0 x1 x2 ⟶ 43cf7.. x0 x1 x2 (proof)
Definition reflexive^reflexive := λ x0 : ι → ι → ο . ∀ x1 . x0 x1 x1
Theorem c3fdc.. : ∀ x0 : ι → ι → ο . reflexive (43cf7.. x0) (proof)
Definition symmetric^symmetric := λ x0 : ι → ι → ο . ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1
Theorem 67843.. : ∀ x0 : ι → ι → ο . symmetric (43cf7.. x0) (proof)
Definition transitive^transitive := λ x0 : ι → ι → ο . ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x2 x3 ⟶ x0 x1 x3
Theorem 4ff83.. : ∀ x0 : ι → ι → ο . transitive (43cf7.. x0) (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition eqreln^eqreln := λ x0 : ι → ι → ο . and (and (reflexive x0) (symmetric x0)) (transitive x0)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem a3070.. : ∀ x0 : ι → ι → ο . eqreln (43cf7.. x0) (proof)
Definition per^per := λ x0 : ι → ι → ο . and (symmetric x0) (transitive x0)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 15fc9.. : ∀ x0 : ι → ι → ο . per (43cf7.. x0) (proof)
Theorem 44752.. : ∀ x0 x1 : ι → ι → ο . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3) ⟶ (∀ x2 . x1 x2 x2) ⟶ (∀ x2 x3 . 43cf7.. x0 x2 x3 ⟶ x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 x3 x4 . 43cf7.. x0 x2 x3 ⟶ x1 x2 x3 ⟶ 43cf7.. x0 x3 x4 ⟶ x1 x3 x4 ⟶ x1 x2 x4) ⟶ ∀ x2 x3 . 43cf7.. x0 x2 x3 ⟶ x1 x2 x3 (proof)
Param ap^ap : ι → ι → ι
Definition 3897e.. := λ x0 x1 x2 x3 x4 . ∀ x5 : ι → ι → ο . (∀ x6 . x6 ∈ x0 ⟶ x5 (ap x1 x6) (ap x2 x6)) ⟶ (∀ x6 . x5 x6 x6) ⟶ (∀ x6 x7 . x5 x6 x7 ⟶ x5 x7 x6) ⟶ (∀ x6 x7 x8 . x5 x6 x7 ⟶ x5 x7 x8 ⟶ x5 x6 x8) ⟶ x5 x3 x4
Theorem 11c16.. : ∀ x0 x1 x2 x3 . x3 ∈ x0 ⟶ 3897e.. x0 x1 x2 (ap x1 x3) (ap x2 x3) (proof)
Theorem bce5d.. : ∀ x0 x1 x2 . reflexive (3897e.. x0 x1 x2) (proof)
Theorem a3a5c.. : ∀ x0 x1 x2 . symmetric (3897e.. x0 x1 x2) (proof)
Theorem e3ced.. : ∀ x0 x1 x2 . transitive (3897e.. x0 x1 x2) (proof)
Theorem d1612.. : ∀ x0 x1 x2 . eqreln (3897e.. x0 x1 x2) (proof)
Theorem d8abc.. : ∀ x0 x1 x2 . per (3897e.. x0 x1 x2) (proof)
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Known iffI^iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known iff_refl^iff_refl : ∀ x0 : ο . iff x0 x0
Known iff_sym^iff_sym : ∀ x0 x1 : ο . iff x0 x1 ⟶ iff x1 x0
Known iff_trans^iff_trans : ∀ x0 x1 x2 : ο . iff x0 x1 ⟶ iff x1 x2 ⟶ iff x0 x2
Theorem 11830.. : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ ∀ x3 . x3 ∈ setexp x1 x0 ⟶ ∀ x4 x5 . 3897e.. x0 x2 x3 x4 x5 ⟶ iff (x4 ∈ x1) (x5 ∈ x1) (proof)
Theorem 1bbdd.. : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ ∀ x3 . x3 ∈ setexp x1 x0 ⟶ ∀ x4 x5 . 3897e.. x0 x2 x3 x4 x5 ⟶ x4 ∈ x1 ⟶ x5 ∈ x1 (proof)
Theorem 77119.. : ∀ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 . x4 ∈ x0 ⟶ x3 (ap x1 x4) (ap x2 x4)) ⟶ (∀ x4 . x3 x4 x4) ⟶ (∀ x4 x5 . 3897e.. x0 x1 x2 x4 x5 ⟶ x3 x4 x5 ⟶ x3 x5 x4) ⟶ (∀ x4 x5 x6 . 3897e.. x0 x1 x2 x4 x5 ⟶ x3 x4 x5 ⟶ 3897e.. x0 x1 x2 x5 x6 ⟶ x3 x5 x6 ⟶ x3 x4 x6) ⟶ ∀ x4 x5 . 3897e.. x0 x1 x2 x4 x5 ⟶ x3 x4 x5 (proof)
Theorem 58f3a.. : ∀ x0 x1 x2 . ∀ x3 : ι → ι . (∀ x4 . x4 ∈ x0 ⟶ x3 (ap x1 x4) = x3 (ap x2 x4)) ⟶ ∀ x4 x5 . 3897e.. x0 x1 x2 x4 x5 ⟶ x3 x4 = x3 x5 (proof)
Param Subq^Subq : ι → ι → ο
Definition MetaCat_coequalizer_p^{coequalizer_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 . λ x10 : ι → ι → ι . and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x1 x4 x5 x6)) (x1 x4 x5 x7)) (x0 x8)) (x1 x5 x8 x9)) (x3 x4 x5 x8 x9 x6 = x3 x4 x5 x8 x9 x7)) (∀ x11 . x0 x11 ⟶ ∀ x12 . x1 x5 x11 x12 ⟶ x3 x4 x5 x11 x12 x6 = x3 x4 x5 x11 x12 x7 ⟶ and (and (x1 x8 x11 (x10 x11 x12)) (x3 x5 x8 x11 (x10 x11 x12) x9 = x12)) (∀ x13 . x1 x8 x11 x13 ⟶ x3 x5 x8 x11 x13 x9 = x12 ⟶ x13 = x10 x11 x12))
Definition MetaCat_coequalizer_struct_p^{coequalizer_constr_p} := λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 : ι → ι → ι → ι → ι . λ x6 : ι → ι → ι → ι → ι → ι → ι . ∀ x7 x8 . x0 x7 ⟶ x0 x8 ⟶ ∀ x9 x10 . x1 x7 x8 x9 ⟶ x1 x7 x8 x10 ⟶ MetaCat_coequalizer_p x0 x1 x2 x3 x7 x8 x9 x10 (x4 x7 x8 x9 x10) (x5 x7 x8 x9 x10) (x6 x7 x8 x9 x10)
Definition HomSet^SetHom := λ x0 x1 x2 . x2 ∈ setexp x1 x0
Param lam^Sigma : ι → (ι → ι) → ι
Definition lam_id^lam_id := λ x0 . lam x0 (λ x1 . x1)
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Param Sep^Sep : ι → (ι → ο) → ι
Param canonical_elt^{canonical_elt} : (ι → ι → ο) → ι → ι
Definition quotient^quotient := λ x0 : ι → ι → ο . λ x1 . and (x0 x1 x1) (x1 = canonical_elt x0 x1)
Known 41253..^and8I : ∀ x0 x1 x2 x3 x4 x5 x6 x7 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7 ⟶ and (and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6) x7
Known Sep_Subq^Sep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1 ⊆ x0
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known canonical_elt_eq^{canonical_elt_eq} : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 x2 . x0 x1 x2 ⟶ canonical_elt x0 x1 = canonical_elt x0 x2
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known SepE1^SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ x2 ∈ x0
Known canonical_elt_rel^{canonical_elt_rel} : ∀ x0 : ι → ι → ο . ∀ x1 . x0 x1 x1 ⟶ x0 x1 (canonical_elt x0 x1)
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Known canonical_elt_idem^{canonical_elt_idem} : ∀ x0 : ι → ι → ο . per x0 ⟶ ∀ x1 . x0 x1 x1 ⟶ canonical_elt x0 x1 = canonical_elt x0 (canonical_elt x0 x1)
Theorem 5bbc1..^{MetaCatSet_coequalizer_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 HomSet lam_id (λ x7 x8 x9 . lam_comp x7) x2 x4 x6 ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Definition True^True := ∀ x0 : ο . x0 ⟶ x0
Known TrueI^TrueI : True
Theorem 33046..^{MetaCatSet_coequalizer} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p (λ x6 . True) HomSet lam_id (λ x6 x7 x8 . lam_comp x6) x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known 6aa34..^{UnivOf_Subq_closed} : ∀ x0 x1 . x1 ∈ prim6 x0 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x2 ∈ prim6 x0
Theorem ef69d..^{MetaCatHFSet_coequalizer} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p (λ x6 . x6 ∈ prim6 0) HomSet lam_id (λ x6 x7 x8 . lam_comp x6) x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Theorem 04991..^{MetaCatSmallSet_coequalizer} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p (λ x6 . x6 ∈ prim6 (prim6 0)) HomSet lam_id (λ x6 x7 x8 . lam_comp x6) x1 x3 x5 ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Param MetaCat^MetaCat : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Param setsum^setsum : ι → ι → ι
Param MetaCat_pushout_constr_p^{pushout_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο
Param MetaCat_coproduct_constr_p^{coproduct_constr_p} : (ι → ο) → (ι → ι → ι → ο) → (ι → ι) → (ι → ι → ι → ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι → ι → ι → ι) → ο
Known b0aad..^{coproduct_coequalizer_pushout_constr_ex} : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι → ι → ι . MetaCat x0 x1 x2 x3 ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι → ι . MetaCat_coequalizer_struct_p x0 x1 x2 x3 x5 x7 x9 ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p x0 x1 x2 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ ∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . (∀ x8 : ο . (∀ x9 : ι → ι → ι → ι → ι → ι . (∀ x10 : ο . (∀ x11 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p x0 x1 x2 x3 x5 x7 x9 x11 ⟶ x10) ⟶ x10) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4
Known 3c078..^{MetaCatSet_coproduct_gen} : ∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setsum x1 x2)) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι . (∀ x7 : ο . (∀ x8 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p x0 HomSet (λ x9 . lam x9 (λ x10 . x10)) (λ x9 x10 x11 x12 x13 . lam x9 (λ x14 . ap x12 (ap x13 x14))) x2 x4 x6 x8 ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Theorem 8381c..^{MetaCatSet_pushout_gen} : ∀ x0 : ι → ο . MetaCat x0 HomSet lam_id (λ x1 x2 x3 . lam_comp x1) ⟶ (∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2) ⟶ (∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setsum x1 x2)) ⟶ ∀ x1 : ο . (∀ x2 : ι → ι → ι → ι → ι → ι . (∀ x3 : ο . (∀ x4 : ι → ι → ι → ι → ι → ι . (∀ x5 : ο . (∀ x6 : ι → ι → ι → ι → ι → ι . (∀ x7 : ο . (∀ x8 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p x0 HomSet lam_id (λ x9 x10 x11 . lam_comp x9) x2 x4 x6 x8 ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1 (proof)
Known e4125..^MetaCatSet : MetaCat (λ x0 . True) HomSet lam_id (λ x0 x1 x2 . lam_comp x0)
Known c28ea..^{MetaCatSet_coproduct} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p (λ x8 . True) HomSet (λ x8 . lam x8 (λ x9 . x9)) (λ x8 x9 x10 x11 x12 . lam x8 (λ x13 . ap x11 (ap x12 x13))) x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Theorem 15618..^{MetaCatSet_pushout} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p (λ x8 . True) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known 2fb6a..^MetaCatHFSet : MetaCat (λ x0 . x0 ∈ prim6 0) HomSet lam_id (λ x0 x1 x2 . lam_comp x0)
Known 5604f..^{MetaCatHFSet_coproduct} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p (λ x8 . x8 ∈ prim6 0) HomSet (λ x8 . lam x8 (λ x9 . x9)) (λ x8 x9 x10 x11 x12 . lam x8 (λ x13 . ap x11 (ap x12 x13))) x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Theorem bfc42..^{MetaCatHFSet_pushout} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p (λ x8 . x8 ∈ prim6 0) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)
Known 68978..^{MetaCatSmallSet} : MetaCat (λ x0 . x0 ∈ prim6 (prim6 0)) HomSet lam_id (λ x0 x1 x2 . lam_comp x0)
Known 002ee..^{MetaCatSmallSet_coproduct} : ∀ x0 : ο . (∀ x1 : ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι . MetaCat_coproduct_constr_p (λ x8 . x8 ∈ prim6 (prim6 0)) HomSet (λ x8 . lam x8 (λ x9 . x9)) (λ x8 x9 x10 x11 x12 . lam x8 (λ x13 . ap x11 (ap x12 x13))) x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0
Theorem b3083..^{MetaCatSmallSet_pushout} : ∀ x0 : ο . (∀ x1 : ι → ι → ι → ι → ι → ι . (∀ x2 : ο . (∀ x3 : ι → ι → ι → ι → ι → ι . (∀ x4 : ο . (∀ x5 : ι → ι → ι → ι → ι → ι . (∀ x6 : ο . (∀ x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pushout_constr_p (λ x8 . x8 ∈ prim6 (prim6 0)) HomSet lam_id (λ x8 x9 x10 . lam_comp x8) x1 x3 x5 x7 ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0 (proof)