Proofgold Proof

Apply df_ppi__df_mu__df_sgm__df_dchr__df_lgs__df_itv__df_lng__df_trkgc__df_trkgb__df_trkgcb__df_trkge__df_trkgld__df_trkg__df_cgrg__df_ismt__df_leg__df_hlg__df_mir with wceq cstrkgb (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . w3a (wral (λ x3 . wral (λ x4 . wcel (cv x4) (co (cv x3) (cv x3) (cv x2)) ⟶ wceq (cv x3) (cv x4)) (λ x4 . cv x1)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wa (wcel (cv x6) (co (cv x3) (cv x5) (cv x2))) (wcel (cv x7) (co (cv x4) (cv x5) (cv x2))) ⟶ wrex (λ x8 . wa (wcel (cv x8) (co (cv x6) (cv x4) (cv x2))) (wcel (cv x8) (co (cv x7) (cv x3) (cv x2)))) (λ x8 . cv x1)) (λ x7 . cv x1)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wrex (λ x5 . wral (λ x6 . wral (λ x7 . wcel (cv x6) (co (cv x5) (cv x7) (cv x2))) (λ x7 . cv x4)) (λ x6 . cv x3)) (λ x5 . cv x1) ⟶ wrex (λ x5 . wral (λ x6 . wral (λ x7 . wcel (cv x5) (co (cv x6) (cv x7) (cv x2))) (λ x7 . cv x4)) (λ x6 . cv x3)) (λ x5 . cv x1)) (λ x4 . cpw (cv x1))) (λ x3 . cpw (cv x1)))) (cfv (cv x0) citv)) (cfv (cv x0) cbs))).