Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
→
ι
→
ο
be given.
Apply unknownprop_5cef9e5da65ddd9e109279d054792510e640b761edb0ef1727132ba3831beaab with
λ x1 x2 :
(
ι →
ι → ο
)
→ ο
.
x2
x0
⟶
∀ x3 : ο .
(
reflexive_i
x0
⟶
symmetric_i
x0
⟶
transitive_i
x0
⟶
x3
)
⟶
x3
.
The subproof is completed by applying unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with
reflexive_i
x0
,
symmetric_i
x0
,
transitive_i
x0
.
■