Proofgold Proof

pf
Let x0 of type ι be given. Apply unknownprop_b57aaa0595c9092e47a248cd8a6237f8a6af9cb91a6bce97bc95c8f9b7b394f0 with x0, ba9d8.. x0 ⟶ prim1 x0 48ef8... Assume H0: prim1 x0 48ef8.. ⟶ ba9d8.. x0. Assume H1: ba9d8.. x0 ⟶ prim1 x0 48ef8... The subproof is completed by applying H1. ■