Apply df_minmar1__df_cpmat__df_mat2pmat__df_cpmat2mat__df_decpmat__df_pm2mp__df_chpmat__df_top__df_topon__df_topsp__df_bases__df_cld__df_ntr__df_cls__df_nei__df_lp__df_perf__df_cn with wceq cperf (crab (λ x0 . wceq (cfv (cuni (cv x0)) (cfv (cv x0) clp)) (cuni (cv x0))) (λ x0 . ctop)).

Assume H0: wceq cminmar1 (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x0) (λ x3 x4 . cv x0) (λ x3 x4 . cmpt2 (λ x5 x6 . cv x0) (λ x5 x6 . cv x0) (λ x5 x6 . cif (wceq (cv x5) (cv x3)) (cif (wceq (cv x6) (cv x4)) (cfv (cv x1) cur) (cfv (cv x1) c0g)) (co (cv x5) (cv x6) (cv x2))))))).

Assume H1: wceq ccpmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (cfv (cv x5) (cfv (co (cv x3) (cv x4) (cv x2)) cco1)) (cfv (cv x1) c0g)) (λ x5 . cn)) (λ x4 . cv x0)) (λ x3 . cv x0)) (λ x2 . cfv (co (cv x0) (cfv (cv x1) cpl1) cmat) cbs))).

Assume H2: wceq cmat2pmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x0) (λ x3 x4 . cv x0) (λ x3 x4 . cfv (co (cv x3) (cv x4) (cv x2)) (cfv (cfv (cv x1) cpl1) cascl))))).

Assume H3: wceq ccpmat2mat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . co (cv x0) (cv x1) ccpmat) (λ x2 . cmpt2 (λ x3 x4 . cv x0) (λ x3 x4 . cv x0) (λ x3 x4 . cfv cc0 (cfv (co (cv x3) (cv x4) (cv x2)) cco1))))).

Assume H4: wceq cdecpmat (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cn0) (λ x0 x1 . cmpt2 (λ x2 x3 . cdm (cdm (cv x0))) (λ x2 x3 . cdm (cdm (cv x0))) (λ x2 x3 . cfv (cv x1) (cfv (co (cv x2) (cv x3) (cv x0)) cco1)))).

Assume H5: wceq cpm2mp (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) ...).

...

■

Proofgold Proof