Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι → ο be given.
Claim L1: 1beb9.. x0 (09072.. x0 x1)
Apply unknownprop_9d54935732f044f1d7b246839daf8ba348c0537db194a1ea4a9ea98310c4d87f with x0, x1.
The subproof is completed by applying H0.
Claim L2: 80242.. (09072.. x0 x1)
Let x2 of type ο be given.
Assume H2: ∀ x3 . and (ordinal x3) (1beb9.. x3 (09072.. x0 x1)) ⟶ x2.
Apply H2 with x0.
Apply andI with ordinal x0, 1beb9.. x0 (09072.. x0 x1) leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L1.
Apply unknownprop_2c27682abc32e1c8a2160a07043a81afe1f256df4f0472edf3cf11efdcea8609 with 09072.. x0 x1, e4431.. (09072.. x0 x1) = x0 leaving 2 subgoals.
The subproof is completed by applying L2.
Assume H3: ordinal (e4431.. (09072.. x0 x1)).
Assume H4: 1beb9.. (e4431.. (09072.. x0 x1)) (09072.. x0 x1).
Apply unknownprop_58b9911fe66d684a6d40350a803ba9ad994b8c3fb391c59cf63767464366ef65 with 09072.. x0 x1, e4431.. (09072.. x0 x1), x0 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying L1.
■