Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ο
be given.
Assume H0:
∀ x1 .
(
∃ x2 :
ι → ι
.
MetaCat_terminal_p
8b17e..
BinRelnHom
struct_id
struct_comp
x1
x2
)
⟶
x0
.
Apply H0 with
pack_r
0
(
λ x1 x2 .
False
)
.
Let x1 of type
ο
be given.
Assume H1:
∀ x2 :
ι → ι
.
MetaCat_terminal_p
8b17e..
BinRelnHom
struct_id
struct_comp
(
pack_r
0
(
λ x3 x4 .
False
)
)
x2
⟶
x1
.
Apply H1 with
λ x2 .
0
.
The subproof is completed by applying unknownprop_5bb34f24f2cd19372c7320ae989b74f2bde5b45cd80a2a08b7da9db21d137956.
■