Apply df_kgen__df_tx__df_xko__df_kq__df_hmeo__df_hmph__df_fil__df_ufil__df_ufl__df_fm__df_flim__df_flf__df_fcls__df_fcf__df_cnext__df_tmd__df_tgp__df_tsms with wceq ctx (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cfv (crn (cmpt2 (λ x2 x3 . cv x0) (λ x2 x3 . cv x1) (λ x2 x3 . cxp (cv x2) (cv x3)))) ctg)).

Assume H0: wceq ckgen (cmpt (λ x0 . ctop) (λ x0 . crab (λ x1 . wral (λ x2 . wcel (co (cv x0) (cv x2) crest) ccmp ⟶ wcel (cin (cv x1) (cv x2)) (co (cv x0) (cv x2) crest)) (λ x2 . cpw (cuni (cv x0)))) (λ x1 . cpw (cuni (cv x0))))).

Assume H1: wceq ctx (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cfv (crn (cmpt2 (λ x2 x3 . cv x0) (λ x2 x3 . cv x1) (λ x2 x3 . cxp (cv x2) (cv x3)))) ctg)).

Assume H2: wceq cxko (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . cfv (cfv (crn (cmpt2 (λ x2 x3 . crab (λ x4 . wcel (co (cv x1) (cv x4) crest) ccmp) (λ x4 . cpw (cuni (cv x1)))) (λ x2 x3 . cv x0) (λ x2 x3 . crab (λ x4 . wss (cima (cv x4) (cv x2)) (cv x3)) (λ x4 . co (cv x1) (cv x0) ccn)))) cfi) ctg)).

Assume H3: wceq ckq (cmpt (λ x0 . ctop) (λ x0 . co (cv x0) (cmpt (λ x1 . cuni (cv x0)) (λ x1 . crab (λ x2 . wcel (cv x1) (cv x2)) (λ x2 . cv x0))) cqtop)).

Assume H4: wceq chmeo (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . crab (λ x2 . wcel (ccnv (cv x2)) (co (cv x1) (cv x0) ccn)) (λ x2 . co (cv x0) (cv x1) ccn))).

Assume H5: wceq chmph (cima (ccnv chmeo) (cdif cvv c1o)).

Assume H6: wceq cfil (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wne (cin (cv x1) (cpw (cv x2))) c0 ⟶ wcel (cv x2) (cv x1)) (λ x2 . cpw (cv x0))) (λ x1 . cfv (cv x0) cfbas))).

Assume H7: wceq cufil (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wo (wcel (cv x2) (cv x1)) ...) ...) ...)).

...

■

Proofgold Proof