Apply df_preset__df_drs__df_poset__df_plt__df_lub__df_glb__df_join__df_meet__df_toset__df_p0__df_p1__df_lat__df_clat__df_odu__df_ipo__df_dlat__df_ps__df_tsr with wceq ctos (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wo (wbr (cv x3) (cv x4) (cv x2)) (wbr (cv x4) (cv x3) (cv x2))) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cple)) (cfv (cv x0) cbs)) (λ x0 . cpo)).

Assume H0: wceq cpreset (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wa (wbr (cv x3) (cv x3) (cv x2)) (wa (wbr (cv x3) (cv x4) (cv x2)) (wbr (cv x4) (cv x5) (cv x2)) ⟶ wbr (cv x3) (cv x5) (cv x2))) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cple)) (cfv (cv x0) cbs))).

Assume H1: wceq cdrs (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wa (wne (cv x1) c0) (wral (λ x3 . wral (λ x4 . wrex (λ x5 . wa (wbr (cv x3) (cv x5) (cv x2)) (wbr (cv x4) (cv x5) (cv x2))) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1))) (cfv (cv x0) cple)) (cfv (cv x0) cbs)) (λ x0 . cpreset)).

Assume H2: wceq cpo (cab (λ x0 . wex (λ x1 . wex (λ x2 . w3a (wceq (cv x1) (cfv (cv x0) cbs)) (wceq (cv x2) (cfv (cv x0) cple)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . w3a (wbr (cv x3) (cv x3) (cv x2)) (wa (wbr (cv x3) (cv x4) (cv x2)) (wbr (cv x4) (cv x3) (cv x2)) ⟶ wceq (cv x3) (cv x4)) (wa (wbr (cv x3) (cv x4) (cv x2)) (wbr (cv x4) (cv x5) (cv x2)) ⟶ wbr (cv x3) (cv x5) (cv x2))) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)))))).

Assume H3: wceq cplt (cmpt ... ...).

...

■

Proofgold Proof