Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. The subproof is completed by applying unknownprop_0d4755c50267998d498b9b7c355e3836657dd91dd0e6bc0c3dd1155cde3ed900 with 4ae4a.. (4ae4a.. 4a7ef..), λ x2 . If_i (x2 = 4a7ef..) x0 x1. ■