Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι → ι → ο be given. The subproof is completed by applying pack_b_b_e_e_4_eq2 with field0 x0, field1b x0, field2b x0, field4 x0, RealsStruct_one x0, λ x2 x3 . x1 x3 x2. ■