Apply df_trg__df_tdrg__df_tlm__df_tvc__df_ust__df_utop__df_uss__df_usp__df_tus__df_ucn__df_cfilu__df_cusp__df_xms__df_ms__df_tms__df_nm__df_ngp__df_tng with wceq cutop (cmpt (λ x0 . cuni (crn cust)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wss (cima (cv x3) (csn (cv x2))) (cv x1)) (λ x3 . cv x0)) (λ x2 . cv x1)) (λ x1 . cpw (cdm (cuni (cv x0)))))).

Assume H0: wceq ctrg (crab (λ x0 . wcel (cfv (cv x0) cmgp) ctmd) (λ x0 . cin ctgp crg)).

Assume H1: wceq ctdrg (crab (λ x0 . wcel (co (cfv (cv x0) cmgp) (cfv (cv x0) cui) cress) ctgp) (λ x0 . cin ctrg cdr)).

Assume H2: wceq ctlm (crab (λ x0 . wa (wcel (cfv (cv x0) csca) ctrg) (wcel (cfv (cv x0) cscaf) (co (co (cfv (cfv (cv x0) csca) ctopn) (cfv (cv x0) ctopn) ctx) (cfv (cv x0) ctopn) ccn))) (λ x0 . cin ctmd clmod)).

Assume H3: wceq ctvc (crab (λ x0 . wcel (cfv (cv x0) csca) ctdrg) (λ x0 . ctlm)).

Assume H4: wceq cust (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . w3a (wss (cv x1) (cpw (cxp (cv x0) (cv x0)))) (wcel (cxp (cv x0) (cv x0)) (cv x1)) (wral (λ x2 . w3a (wral (λ x3 . wss (cv x2) (cv x3) ⟶ wcel (cv x3) (cv x1)) (λ x3 . cpw (cxp (cv x0) (cv x0)))) (wral (λ x3 . wcel (cin (cv x2) (cv x3)) (cv x1)) (λ x3 . cv x1)) (w3a (wss (cres cid (cv x0)) (cv x2)) (wcel (ccnv (cv x2)) (cv x1)) (wrex (λ x3 . wss (ccom (cv x3) (cv x3)) (cv x2)) (λ x3 . cv x1)))) (λ x2 . cv x1))))).

Assume H5: wceq cutop (cmpt (λ x0 . cuni (crn cust)) (λ x0 . crab (λ x1 . wral (λ x2 . wrex (λ x3 . wss (cima (cv x3) (csn (cv x2))) (cv x1)) (λ x3 . cv x0)) (λ x2 . cv x1)) (λ x1 . cpw (cdm (cuni (cv x0)))))).

Assume H6: wceq cuss ....

...

■

Proofgold Proof