Proofgold Proof

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