Apply df_mpq__df_ltpq__df_enq__df_nq__df_erq__df_plq__df_mq__df_1nq__df_rq__df_ltnq__df_np__df_1p__df_plp__df_mp__df_ltp__df_enr__df_nr__df_plr with wceq cmp (cmpt2 (λ x0 x1 . cnp) (λ x0 x1 . cnp) (λ x0 x1 . cab (λ x2 . wrex (λ x3 . wrex (λ x4 . wceq (cv x2) (co (cv x3) (cv x4) cmq)) (λ x4 . cv x1)) (λ x3 . cv x0)))).

Assume H0: wceq cmpq (cmpt2 (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cxp cnpi cnpi) (λ x0 x1 . cop (co (cfv (cv x0) c1st) (cfv (cv x1) c1st) cmi) (co (cfv (cv x0) c2nd) (cfv (cv x1) c2nd) cmi))).

Assume H1: wceq cltpq (copab (λ x0 x1 . wa (wa (wcel (cv x0) (cxp cnpi cnpi)) (wcel (cv x1) (cxp cnpi cnpi))) (wbr (co (cfv (cv x0) c1st) (cfv (cv x1) c2nd) cmi) (co (cfv (cv x1) c1st) (cfv (cv x0) c2nd) cmi) clti))).

Assume H2: wceq ceq (copab (λ x0 x1 . wa (wa (wcel (cv x0) (cxp cnpi cnpi)) (wcel (cv x1) (cxp cnpi cnpi))) (wex (λ x2 . wex (λ x3 . wex (λ x4 . wex (λ x5 . wa (wa (wceq (cv x0) (cop (cv x2) (cv x3))) (wceq (cv x1) (cop (cv x4) (cv x5)))) (wceq (co (cv x2) (cv x5) cmi) (co (cv x3) (cv x4) cmi))))))))).

Assume H3: wceq cnq (crab (λ x0 . wral (λ x1 . wbr (cv x0) (cv x1) ceq ⟶ wn (wbr (cfv (cv x1) c2nd) (cfv (cv x0) c2nd) clti)) (λ x1 . cxp cnpi cnpi)) (λ x0 . cxp cnpi cnpi)).

Assume H4: wceq cerq (cin ceq (cxp (cxp cnpi cnpi) cnq)).

Assume H5: wceq cplq (cres (ccom cerq cplpq) (cxp cnq cnq)).

Assume H6: wceq cmq (cres (ccom cerq cmpq) (cxp cnq cnq)).

Assume H7: wceq c1q (cop c1o c1o).

Assume H8: wceq crq (cima (ccnv cmq) (csn c1q)).

Assume H9: wceq cltq (cin cltpq (cxp cnq cnq)).

Assume H10: wceq cnp (cab (λ x0 . wa (wa (wpss c0 (cv ...)) ...) ...)).

...

■

Proofgold Proof