Apply df_dir__df_tail__df_plusf__df_mgm__df_sgrp__df_mnd__df_mhm__df_submnd__df_frmd__df_vrmd__df_grp__df_minusg__df_sbg__df_mulg__df_subg__df_nsg__df_eqg__df_ghm with wceq cgrp (crab (λ x0 . wral (λ x1 . wrex (λ x2 . wceq (co (cv x2) (cv x1) (cfv (cv x0) cplusg)) (cfv (cv x0) c0g)) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs)) (λ x0 . cmnd)).

Assume H0: wceq cdir (cab (λ x0 . wa (wa (wrel (cv x0)) (wss (cres cid (cuni (cuni (cv x0)))) (cv x0))) (wa (wss (ccom (cv x0) (cv x0)) (cv x0)) (wss (cxp (cuni (cuni (cv x0))) (cuni (cuni (cv x0)))) (ccom (ccnv (cv x0)) (cv x0)))))).

Assume H1: wceq ctail (cmpt (λ x0 . cdir) (λ x0 . cmpt (λ x1 . cuni (cuni (cv x0))) (λ x1 . cima (cv x0) (csn (cv x1))))).

Assume H2: wceq cplusf (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . co (cv x1) (cv x2) (cfv (cv x0) cplusg)))).

Assume H3: wceq cmgm (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wcel (co (cv x3) (cv x4) (cv x2)) (cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs))).

Assume H4: wceq csgrp (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (co (co (cv x3) (cv x4) (cv x2)) (cv x5) (cv x2)) (co (cv x3) (co (cv x4) (cv x5) (cv x2)) (cv x2))) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . cmgm)).

Assume H5: wceq cmnd (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wrex (λ x3 . wral (λ x4 . wa (wceq (co (cv x3) (cv x4) (cv x2)) (cv x4)) (wceq (co (cv x4) (cv x3) (cv x2)) (cv x4))) ...) ...) ...) ...) ...).

...

■

Proofgold Proof