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. Let x4 of type ο be given. The subproof is completed by applying orIR with or (or (or x0 x1) x2) x3, x4. ■