Proofgold Proof

Apply df_ordt__df_xrs__df_qtop__df_imas__df_qus__df_xps__df_mre__df_mrc__df_mri__df_acs__df_cat__df_cid__df_homf__df_comf__df_oppc__df_mon__df_epi__df_sect with wceq ccat (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wa (wrex (λ x5 . wral (λ x6 . wa (wral (λ x7 . wceq (co (cv x5) (cv x7) (co (cop (cv x6) (cv x4)) (cv x4) (cv x3))) (cv x7)) (λ x7 . co (cv x6) (cv x4) (cv x2))) (wral (λ x7 . wceq (co (cv x7) (cv x5) (co (cop (cv x4) (cv x4)) (cv x6) (cv x3))) (cv x7)) (λ x7 . co (cv x4) (cv x6) (cv x2)))) (λ x6 . cv x1)) (λ x5 . co (cv x4) (cv x4) (cv x2))) (wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wa (wcel (co (cv x8) (cv x7) (co (cop (cv x4) (cv x5)) (cv x6) (cv x3))) (co (cv x4) (cv x6) (cv x2))) (wral (λ x9 . wral (λ x10 . wceq (co (co (cv x10) (cv x8) (co (cop (cv x5) (cv x6)) (cv x9) (cv x3))) (cv x7) (co (cop (cv x4) (cv x5)) (cv x9) (cv x3))) (co (cv x10) (co (cv x8) (cv x7) (co (cop (cv x4) (cv x5)) (cv x6) (cv x3))) (co (cop (cv x4) (cv x6)) (cv x9) (cv x3)))) (λ x10 . co (cv x6) (cv x9) (cv x2))) (λ x9 . cv x1))) (λ x8 . co (cv x5) (cv x6) (cv x2))) (λ x7 . co (cv x4) (cv x5) (cv x2))) (λ x6 . cv x1)) (λ x5 . cv x1))) (λ x4 . cv x1)) (cfv (cv x0) cco)) (cfv (cv x0) chom)) (cfv (cv x0) cbs))).