Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply unknownprop_6309f32475bcfc5c43876e0ea3ff21ee2bbf448bf4d934c2220eba39b2727bd5 with x0, 0, λ x1 x2 . x2 = x0.
The subproof is completed by applying unknownprop_5ae672e89a21a9442264a67242475d56fabcbad0c93d631a43c5409e42b4f940 with x0.