Apply ax_cc__ax_dc__ax_ac__ax_ac2__df_gch__df_wina__df_ina__df_wun__df_wunc__df_tsk__df_gru__ax_groth__df_tskm__df_ni__df_pli__df_mi__df_lti__df_plpq with wceq ctsk (cab (λ x0 . wa (wral (λ x1 . wa (wss (cpw (cv x1)) (cv x0)) (wrex (λ x2 . wss (cpw (cv x1)) (cv x2)) (λ x2 . cv x0))) (λ x1 . cv x0)) (wral (λ x1 . wo (wbr (cv x1) (cv x0) cen) (wcel (cv x1) (cv x0))) (λ x1 . cpw (cv x0))))).

Assume H0: ∀ x0 . wbr (cv x0) com cen ⟶ wex (λ x1 . wral (λ x2 . wne (cv x2) c0 ⟶ wcel (cfv (cv x2) (cv x1)) (cv x2)) (λ x2 . cv x0)).

Assume H1: ∀ x0 . wa (wex (λ x1 . wex (λ x2 . wbr (cv x1) (cv x2) (cv x0)))) (wss (crn (cv x0)) (cdm (cv x0))) ⟶ wex (λ x1 . wral (λ x2 . wbr (cfv (cv x2) (cv x1)) (cfv (csuc (cv x2)) (cv x1)) (cv x0)) (λ x2 . com)).

Assume H2: ∀ x0 . wex (λ x1 . ∀ x2 x3 . wa (wcel (cv x2) (cv x3)) (wcel (cv x3) (cv x0)) ⟶ wex (λ x4 . ∀ x5 . wb (wex (λ x6 . wa (wa (wcel (cv x5) (cv x3)) (wcel (cv x3) (cv x6))) (wa (wcel (cv x5) (cv x6)) (wcel (cv x6) (cv x1))))) (wceq (cv x5) (cv x4)))).

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

Assume H4: wceq cgch (cun cfn (cab (λ x0 . ∀ x1 . wn (wa (wbr (cv x0) ... ...) ...)))).

...

■

Proofgold Proof