Search for blocks/addresses/...
Proofgold Proof
pf
Apply andI with
TransSet
48ef8..
,
∀ x0 .
prim1
x0
48ef8..
⟶
TransSet
x0
leaving 2 subgoals.
The subproof is completed by applying unknownprop_4ecbe7e09dcbbaddb8e46b15576d7b7d75e19d6df6a0ed7c29a496384fce3d13.
Let x0 of type
ι
be given.
Assume H0:
prim1
x0
48ef8..
.
Apply ordinal_TransSet with
x0
.
Apply unknownprop_67a9b4da3479f0b3ecc9f46f5080b801e2df28e772a8a9215f9b75577fbd1e20 with
x0
.
Apply unknownprop_03f5f7248b8d06fe27b9a4f75f4e437d5e9b43a9092733e8b3f6dcfe61f5e308 with
x0
.
The subproof is completed by applying H0.
■