Proofgold Proof

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