Apply df_vts__ax_hgt749__ax_ros335__ax_ros336__df_trkg2d__df_afs__df_bnj17__df_bnj14__df_bnj13__df_bnj15__df_bnj18__df_bnj19__ax_7d__ax_8d__ax_9d1__ax_9d2__ax_10d__ax_11d with ∀ x0 x1 x2 : ι → ο . wceq (c_bnj14 x0 x1 x2) (crab (λ x3 . wbr (cv x3) x2 x1) (λ x3 . x0)).

Assume H0: wceq cvts (cmpt2 (λ x0 x1 . co cc cn cmap) (λ x0 x1 . cn0) (λ x0 x1 . cmpt (λ x2 . cc) (λ x2 . csu (co c1 (cv x1) cfz) (λ x3 . co (cfv (cv x3) (cv x0)) (cfv (co (co ci (co c2 cpi cmul) cmul) (co (cv x3) (cv x2) cmul) cmul) ce) cmul)))).

Assume H1: wral (λ x0 . wbr (co (cdc c1 cc0) (cdc c2 c7) cexp) (cv x0) cle ⟶ wrex (λ x1 . wrex (λ x2 . w3a (wral (λ x3 . wbr (cfv (cv x3) (cv x2)) (co c1 (cdp2 cc0 (cdp2 c7 (cdp2 c9 (cdp2 c9 (cdp2 c5 c5))))) cdp) cle) (λ x3 . cn)) (wral (λ x3 . wbr (cfv (cv x3) (cv x1)) (co c1 (cdp2 c4 (cdp2 c1 c4)) cdp) cle) (λ x3 . cn)) (wbr (co (co cc0 (cdp2 cc0 (cdp2 cc0 (cdp2 cc0 (cdp2 c4 (cdp2 c2 (cdp2 c2 (cdp2 c4 c8))))))) cdp) (co (cv x0) c2 cexp) cmul) (citg (λ x3 . co cc0 c1 cioo) (λ x3 . co (co (cfv (cv x3) (co (co cvma (cv x1) (cof cmul)) (cv x0) cvts)) (co (cfv (cv x3) (co (co cvma (cv x2) (cof cmul)) (cv x0) cvts)) c2 cexp) cmul) (cfv (co (co ci (co c2 cpi cmul) cmul) (co (cneg (cv x0)) (cv x3) cmul) cmul) ce) cmul)) cle)) (λ x2 . co (co cc0 cpnf cico) cn cmap)) (λ x1 . co (co cc0 cpnf cico) cn cmap)) (λ x0 . crab (λ x1 . wn (wbr c2 (cv x1) cdvds)) (λ x1 . cz)).

Assume H2: wral (λ x0 . wbr (cfv (cv x0) cchp) (co (co c1 (cdp2 cc0 (cdp2 ... ...)) ...) ... ...) ...) ....

...

■

Proofgold Proof