Search for blocks/addresses/...

Proofgold Proof

pf
Apply functional extensionality with f6917.., aae7a.. 4a7ef...
Let x0 of type ι be given.
Let x1 of type ιιο be given.
The subproof is completed by applying unknownprop_95043111ebf5d0ba1e3a3dbcd59c8bdd5982670104cfa28d6d14c737e5bfd1d7 with x0, λ x2 x3 . x1 x3 x2.