Apply ax_inf2__df_cnf__df_tc__df_r1__df_rank__df_card__df_aleph__df_cf__df_acn__df_ac__df_cda__df_fin1a__df_fin2__df_fin4__df_fin3__df_fin5__df_fin6__df_fin7 with wceq cfin4 (cab (λ x0 . wn (wex (λ x1 . wa (wpss (cv x1) (cv x0)) (wbr (cv x1) (cv x0) cen))))).

Assume H0: wex (λ x0 . wa (wex (λ x1 . wa (wcel (cv x1) (cv x0)) (∀ x2 . wn (wcel (cv x2) (cv x1))))) (∀ x1 . wcel (cv x1) (cv x0) ⟶ wex (λ x2 . wa (wcel (cv x2) (cv x0)) (∀ x3 . wb (wcel (cv x3) (cv x2)) (wo (wcel (cv x3) (cv x1)) (wceq (cv x3) (cv x1))))))).

Assume H1: wceq ccnf (cmpt2 (λ x0 x1 . con0) (λ x0 x1 . con0) (λ x0 x1 . cmpt (λ x2 . crab (λ x3 . wbr (cv x3) c0 cfsupp) (λ x3 . co (cv x0) (cv x1) cmap)) (λ x2 . csb (coi (co (cv x2) c0 csupp) cep) (λ x3 . cfv (cdm (cv x3)) (cseqom (cmpt2 (λ x4 x5 . cvv) (λ x4 x5 . cvv) (λ x4 x5 . co (co (co (cv x0) (cfv (cv x4) (cv x3)) coe) (cfv (cfv (cv x4) (cv x3)) (cv x2)) comu) (cv x5) coa)) c0))))).

Assume H2: wceq ctc (cmpt (λ x0 . cvv) (λ x0 . cint (cab (λ x1 . wa (wss (cv x0) (cv x1)) (wtr (cv x1)))))).

Assume H3: wceq cr1 (crdg (cmpt (λ x0 . cvv) (λ x0 . cpw (cv x0))) c0).

Assume H4: wceq crnk (cmpt (λ x0 . cvv) (λ x0 . cint (crab (λ x1 . wcel (cv x0) (cfv (csuc (cv x1)) cr1)) (λ x1 . con0)))).

Assume H5: wceq ccrd (cmpt (λ x0 . cvv) (λ x0 . cint (crab (λ x1 . wbr (cv x1) (cv x0) cen) (λ x1 . con0)))).

Assume H6: wceq cale (crdg char com).

Assume H7: wceq ccf (cmpt (λ x0 . con0) (λ x0 . cint (cab (λ x1 . wex (λ x2 . wa (wceq (cv x1) (cfv (cv x2) ccrd)) (wa (wss (cv x2) (cv x0)) (wral (λ x3 . wrex (λ x4 . wss (cv x3) (cv x4)) (λ x4 . cv x2)) (λ x3 . cv x0)))))))).

...

■

Proofgold Proof