Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ο be given.
Assume H0: ∀ x1 . (∃ x2 : ι → ι . ∃ x3 x4 . ∃ x5 : ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p 8b17e.. BinRelnHom struct_id struct_comp x1 x2 x3 x4 x5 x6) ⟶ x0.
Apply H0 with pack_r 0 (λ x1 x2 . False).
Let x1 of type ο be given.
Assume H1: ∀ x2 : ι → ι . (∃ x3 x4 . ∃ x5 : ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p 8b17e.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x7 x8 . False)) x2 x3 x4 x5 x6) ⟶ x1.
Apply H1 with λ x2 . 0.
Let x2 of type ο be given.
Assume H2: ∀ x3 . (∃ x4 . ∃ x5 : ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p 8b17e.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x7 x8 . False)) (λ x7 . 0) x3 x4 x5 x6) ⟶ x2.
Apply H2 with pack_r 0 (λ x3 x4 . False).
Let x3 of type ο be given.
Assume H3: ∀ x4 . (∃ x5 : ι → ι → ι → ι . ∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p 8b17e.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x7 x8 . False)) (λ x7 . 0) (pack_r 0 (λ x7 x8 . False)) x4 x5 x6) ⟶ x3.
Apply H3 with 0.
Let x4 of type ο be given.
Assume H4: ∀ x5 : ι → ι → ι → ι . (∃ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p 8b17e.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x7 x8 . False)) (λ x7 . 0) (pack_r 0 (λ x7 x8 . False)) 0 x5 x6) ⟶ x4.
Apply H4 with λ x5 x6 x7 . 0.
Let x5 of type ο be given.
Assume H5: ∀ x6 : ι → ι → ι → ι → ι → ι → ι . MetaCat_subobject_classifier_p 8b17e.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x7 x8 . False)) (λ x7 . 0) (pack_r 0 (λ x7 x8 . False)) 0 (λ x7 x8 x9 . 0) x6 ⟶ x5.
Apply H5 with λ x6 x7 x8 x9 x10 x11 . 0.
Claim L6: ...
...
Apply and4I with MetaCat_terminal_p 8b17e.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x6 x7 . False)) (λ x6 . 0), 8b17e.. (pack_r 0 (λ x6 x7 . False)), BinRelnHom (pack_r 0 (λ x6 x7 . False)) (pack_r 0 (λ x6 x7 . False)) 0, ∀ x6 x7 x8 . MetaCat_monic_p 8b17e.. BinRelnHom struct_id struct_comp x6 x7 x8 ⟶ and (BinRelnHom x7 (pack_r 0 (λ x9 x10 . False)) 0) (MetaCat_pullback_p 8b17e.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x9 x10 . False)) x7 (pack_r 0 (λ x9 x10 . False)) 0 0 x6 0 x8 (λ x9 x10 x11 . 0)) leaving 4 subgoals.
The subproof is completed by applying unknownprop_5bb34f24f2cd19372c7320ae989b74f2bde5b45cd80a2a08b7da9db21d137956.
The subproof is completed by applying L6.
Apply unknownprop_5d29dee76dbe631c3e61c3da6506dfaf505efc5a4aa6bec582f8fe5c402e18fa with pack_r 0 (λ x6 x7 . False), pack_r 0 (λ x6 x7 . False) leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L6.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H7: MetaCat_monic_p 8b17e.. BinRelnHom struct_id struct_comp x6 x7 x8.
Apply H7 with and (BinRelnHom x7 (pack_r 0 (λ x9 x10 . False)) 0) (MetaCat_pullback_p 8b17e.. BinRelnHom struct_id struct_comp (pack_r 0 (λ x9 x10 . False)) x7 (pack_r 0 (λ x9 x10 . False)) 0 0 x6 0 x8 ...).
...
■