Apply df_ordt__df_xrs__df_qtop__df_imas__df_qus__df_xps__df_mre__df_mrc__df_mri__df_acs__df_cat__df_cid__df_homf__df_comf__df_oppc__df_mon__df_epi__df_sect with wceq cqtop (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wcel (cin (cima (ccnv (cv x1)) (cv x2)) (cuni (cv x0))) (cv x0)) (λ x2 . cpw (cima (cv x1) (cuni (cv x0)))))).

Assume H0: wceq cordt (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cun (csn (cdm (cv x0))) (crn (cun (cmpt (λ x1 . cdm (cv x0)) (λ x1 . crab (λ x2 . wn (wbr (cv x2) (cv x1) (cv x0))) (λ x2 . cdm (cv x0)))) (cmpt (λ x1 . cdm (cv x0)) (λ x1 . crab (λ x2 . wn (wbr (cv x1) (cv x2) (cv x0))) (λ x2 . cdm (cv x0))))))) cfi) ctg)).

Assume H1: wceq cxrs (cun (ctp (cop (cfv cnx cbs) cxr) (cop (cfv cnx cplusg) cxad) (cop (cfv cnx cmulr) cxmu)) (ctp (cop (cfv cnx cts) (cfv cle cordt)) (cop (cfv cnx cple) cle) (cop (cfv cnx cds) (cmpt2 (λ x0 x1 . cxr) (λ x0 x1 . cxr) (λ x0 x1 . cif (wbr (cv x0) (cv x1) cle) (co (cv x1) (cxne (cv x0)) cxad) (co (cv x0) (cxne (cv x1)) cxad)))))).

Assume H2: wceq cqtop (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wcel (cin (cima (ccnv (cv x1)) (cv x2)) (cuni (cv x0))) (cv x0)) (λ x2 . cpw (cima (cv x1) (cuni (cv x0)))))).

Assume H3: wceq cimas (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cfv (cv x1) cbs) (λ x2 . cun (cun (ctp (cop (cfv cnx cbs) (crn (cv x0))) (cop (cfv cnx cplusg) (ciun (λ x3 . cv x2) (λ x3 . ciun (λ x4 . cv x2) (λ x4 . csn (cop (cop (cfv (cv x3) (cv x0)) (cfv (cv x4) (cv x0))) (cfv (co (cv x3) (cv x4) (cfv (cv x1) cplusg)) (cv x0))))))) (cop (cfv cnx cmulr) ...)) ...) ...))).

...

■

Proofgold Proof