Search for blocks/addresses/...
Proofgold Proposition
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι →
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 :
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat
x0
x1
x2
x3
⟶
(
∃ x4 x6 :
ι →
ι →
ι →
ι → ι
.
∃ x8 :
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_coequalizer_buggy_struct_p
x0
x1
x2
x3
x4
x6
x8
)
⟶
(
∃ x4 x6 x8 :
ι →
ι → ι
.
∃ x10 :
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_coproduct_constr_p
x0
x1
x2
x3
x4
x6
x8
x10
)
⟶
∃ x4 x6 x8 :
ι →
ι →
ι →
ι →
ι → ι
.
∃ x10 :
ι →
ι →
ι →
ι →
ι →
ι →
ι →
ι → ι
.
MetaCat_pushout_buggy_constr_p
x0
x1
x2
x3
x4
x6
x8
x10
type
prop
theory
HotG
name
-
proof
PUNFE..
Megalodon
-
proofgold address
TMFnT..
creator
9568
PrCx1..
/
c23c0..
owner
9568
PrCx1..
/
c23c0..
term root
bc6a6..