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 : ι → ο . 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 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) ...) ...)).

...

■

Proofgold Proof