Apply df_lmat__df_cref__df_ldlf__df_pcmp__df_metid__df_pstm__df_hcmp__df_qqh__df_rrh__df_rrext__df_xrh__df_mntop__df_ind__df_esum__df_ofc__df_siga__df_sigagen__df_brsiga with ∀ x0 x1 : ι → ι → ο . wceq (cesum (λ x2 . x0 x2) (λ x2 . x1 x2)) (cuni (co (co cxrs (co cc0 cpnf cicc) cress) (cmpt (λ x2 . x0 x2) (λ x2 . x1 x2)) ctsu)).

Assume H0: wceq clmat (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . co c1 (cfv (cv x0) chash) cfz) (λ x1 x2 . co c1 (cfv (cfv cc0 (cv x0)) chash) cfz) (λ x1 x2 . cfv (co (cv x2) c1 cmin) (cfv (co (cv x1) c1 cmin) (cv x0))))).

Assume H1: ∀ x0 : ι → ο . wceq (ccref x0) (crab (λ x1 . wral (λ x2 . wceq (cuni (cv x1)) (cuni (cv x2)) ⟶ wrex (λ x3 . wbr (cv x3) (cv x2) cref) (λ x3 . cin (cpw (cv x1)) x0)) (λ x2 . cpw (cv x1))) (λ x1 . ctop)).

Assume H2: wceq cldlf (ccref (cab (λ x0 . wbr (cv x0) com cdom))).

Assume H3: wceq cpcmp (cab (λ x0 . wcel (cv x0) (ccref (cfv (cv x0) clocfin)))).

Assume H4: wceq cmetid (cmpt (λ x0 . cuni (crn cpsmet)) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (cdm (cdm (cv x0)))) (wcel (cv x2) (cdm (cdm (cv x0))))) (wceq (co (cv x1) (cv x2) (cv x0)) cc0)))).

Assume H5: wceq cpstm (cmpt (λ x0 . cuni (crn cpsmet)) (λ x0 . cmpt2 (λ x1 x2 . cqs (cdm (cdm (cv x0))) (cfv (cv x0) cmetid)) (λ x1 x2 . cqs (cdm (cdm (cv x0))) (cfv (cv x0) cmetid)) (λ x1 x2 . cuni (cab (λ x3 . wrex (λ x4 . wrex (λ x5 . wceq (cv x3) (co (cv x4) (cv x5) (cv x0))) (λ x5 . cv x2)) (λ x4 . cv x1)))))).

Assume H6: wceq chcmp (copab (λ x0 x1 . w3a (wa (wcel (cv x0) (cuni (crn cust))) (wcel (cv x1) ccusp)) (wceq (co (cfv (cv x1) cuss) (cdm (cuni (cv x0))) crest) (cv x0)) (wceq (cfv (cdm (cuni (cv x0))) (cfv ... ...)) ...))).

...

■

Proofgold Proof