Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: MetaCat x0 HomSet (λ x1 . lam_id x1) (λ x1 x2 x3 x4 x5 . lam_comp x1 x4 x5).
Assume H1: ∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2.
Assume H2: ∀ x1 . x0 x1 ⟶ ∀ x2 . x0 x2 ⟶ x0 (setprod x1 x2).
Claim L3: ∃ x1 x2 : ι → ι → ι → ι → ι . ∃ x3 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p x0 HomSet (λ x4 . lam_id x4) (λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8) x1 x2 x3
Apply unknownprop_ddd882da3ecb083533c5169d9ba0d589c2851738e8d8ddd48b103e4363b8bfa8 with x0.
The subproof is completed by applying H1.
Claim L4: ∃ x1 x2 x3 : ι → ι → ι . ∃ x4 : ι → ι → ι → ι → ι → ι . MetaCat_product_constr_p x0 HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) x1 x2 x3 x4
Apply unknownprop_2d427e86e80080bca0cd1cdb7569c48ac3ebc7f720e53d0aef56ae9082c9d013 with x0.
The subproof is completed by applying H2.
Apply unknownprop_9a59ecd7e83aeba0d4be9a32b55c5c57c6083b63a3b259e3f5889e4923a1993d with x0, HomSet, λ x1 . lam_id x1, λ x1 x2 x3 x4 x5 . lam_comp x1 x4 x5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
■