Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: x0 = x1 ⟶ ∀ x2 : ο . x2. Assume H1: 4ae4a.. x0 = 4ae4a.. x1. Apply H0. Apply unknownprop_684cb1205e38822a7a824f8a0440cb0f546e66d657860b857331eee8a38df013 with x0, x1. The subproof is completed by applying H1. ■