Apply df_polarityN__df_psubclN__df_lhyp__df_laut__df_watsN__df_pautN__df_ldil__df_ltrn__df_dilN__df_trnN__df_trl__df_tgrp__df_tendo__df_edring_rN__df_edring__df_dveca__df_disoa__df_dvech with wceq cldil (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . crab (λ x2 . wral (λ x3 . wbr (cv x3) (cv x1) (cfv (cv x0) cple) ⟶ wceq (cfv (cv x3) (cv x2)) (cv x3)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) claut)))).

Assume H0: wceq cpolN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) catm)) (λ x1 . cin (cfv (cv x0) catm) (ciin (λ x2 . cv x1) (λ x2 . cfv (cfv (cv x2) (cfv (cv x0) coc)) (cfv (cv x0) cpmap)))))).

Assume H1: wceq cpscN (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wa (wss (cv x1) (cfv (cv x0) catm)) (wceq (cfv (cfv (cv x1) (cfv (cv x0) cpolN)) (cfv (cv x0) cpolN)) (cv x1))))).

Assume H2: wceq clh (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wbr (cv x1) (cfv (cv x0) cp1) (cfv (cv x0) ccvr)) (λ x1 . cfv (cv x0) cbs))).

Assume H3: wceq claut (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wa (wf1o (cfv (cv x0) cbs) (cfv (cv x0) cbs) (cv x1)) (wral (λ x2 . wral (λ x3 . wb (wbr (cv x2) (cv x3) (cfv (cv x0) cple)) (wbr (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)) (cfv (cv x0) cple))) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) cbs))))).

Assume H4: wceq cwpointsN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) catm) (λ x1 . cdif (cfv (cv x0) catm) (cfv (csn (cv x1)) (cfv (cv x0) cpolN))))).

Assume H5: wceq cpautN (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wa (wf1o (cfv (cv x0) cpsubsp) (cfv (cv x0) cpsubsp) (cv x1)) (wral (λ x2 . wral (λ x3 . wb (wss (cv x2) (cv ...)) ...) ...) ...)))).

...

■

Proofgold Proof