Apply df_oposet__df_cmtN__df_ol__df_oml__df_covers__df_ats__df_atl__df_cvlat__df_hlat__df_llines__df_lplanes__df_lvols__df_lines__df_pointsN__df_psubsp__df_pmap__df_padd__df_pclN with wceq cpmap (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . crab (λ x2 . wbr (cv x2) (cv x1) (cfv (cv x0) cple)) (λ x2 . cfv (cv x0) catm)))).

Assume H0: wceq cops (crab (λ x0 . wa (wa (wcel (cfv (cv x0) cbs) (cdm (cfv (cv x0) club))) (wcel (cfv (cv x0) cbs) (cdm (cfv (cv x0) cglb)))) (wex (λ x1 . wa (wceq (cv x1) (cfv (cv x0) coc)) (wral (λ x2 . wral (λ x3 . w3a (w3a (wcel (cfv (cv x2) (cv x1)) (cfv (cv x0) cbs)) (wceq (cfv (cfv (cv x2) (cv x1)) (cv x1)) (cv x2)) (wbr (cv x2) (cv x3) (cfv (cv x0) cple) ⟶ wbr (cfv (cv x3) (cv x1)) (cfv (cv x2) (cv x1)) (cfv (cv x0) cple))) (wceq (co (cv x2) (cfv (cv x2) (cv x1)) (cfv (cv x0) cjn)) (cfv (cv x0) cp1)) (wceq (co (cv x2) (cfv (cv x2) (cv x1)) (cfv (cv x0) cmee)) (cfv (cv x0) cp0))) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) cbs))))) (λ x0 . cpo)).

Assume H1: wceq ccmtN (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . w3a (wcel (cv x1) (cfv (cv x0) cbs)) (wcel (cv x2) (cfv (cv x0) cbs)) (wceq (cv x1) (co (co (cv x1) (cv x2) (cfv (cv x0) cmee)) (co (cv x1) (cfv (cv x2) (cfv (cv x0) coc)) (cfv (cv x0) cmee)) (cfv (cv x0) cjn)))))).

Assume H2: wceq col (cin clat cops).

Assume H3: wceq coml (crab (λ x0 . wral (λ x1 . wral (λ x2 . ... ⟶ wceq (cv x2) (co (cv x1) (co (cv x2) (cfv (cv x1) (cfv (cv x0) coc)) (cfv (cv x0) cmee)) (cfv ... ...))) ...) ...) ...).

...

■

Proofgold Proof