Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Claim L1: ordinal (e4431.. x0)
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with x0.
The subproof is completed by applying H0.
Claim L2: ordinal (4ae4a.. (e4431.. x0))
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with e4431.. x0.
The subproof is completed by applying L1.
Claim L3: prim1 x0 (56ded.. (4ae4a.. (e4431.. x0)))
Apply unknownprop_55be23921c8e687561ab6e9faf36ed3618fa021f01ef196ba95aa8fcda0b83ee with x0.
The subproof is completed by applying H0.
Apply unknownprop_79d60d071a58f118f5f172b6182997ae74bdacf356a0626f4cc57773fca49670 with 4ae4a.. (e4431.. x0), x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.