Proofgold Asset

Known df_polarityN__df_psubclN__df_lhyp__df_laut__df_watsN__df_pautN__df_ldil__df_ltrn__df_dilN__df_trnN__df_trl__df_tgrp__df_tendo__df_edring_rN__df_edring__df_dveca__df_disoa__df_dvech : ∀ x0 : ο . (wceq cpolN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) catm)) (λ x2 . cin (cfv (cv x1) catm) (ciin (λ x3 . cv x2) (λ x3 . cfv (cfv (cv x3) (cfv (cv x1) coc)) (cfv (cv x1) cpmap)))))) ⟶ wceq cpscN (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wa (wss (cv x2) (cfv (cv x1) catm)) (wceq (cfv (cfv (cv x2) (cfv (cv x1) cpolN)) (cfv (cv x1) cpolN)) (cv x2))))) ⟶ wceq clh (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wbr (cv x2) (cfv (cv x1) cp1) (cfv (cv x1) ccvr)) (λ x2 . cfv (cv x1) cbs))) ⟶ wceq claut (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wa (wf1o (cfv (cv x1) cbs) (cfv (cv x1) cbs) (cv x2)) (wral (λ x3 . wral (λ x4 . wb (wbr (cv x3) (cv x4) (cfv (cv x1) cple)) (wbr (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x1) cple))) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) cbs))))) ⟶ wceq cwpointsN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) catm) (λ x2 . cdif (cfv (cv x1) catm) (cfv (csn (cv x2)) (cfv (cv x1) cpolN))))) ⟶ wceq cpautN (cmpt (λ x1 . cvv) (λ x1 . cab (λ x2 . wa (wf1o (cfv (cv x1) cpsubsp) (cfv (cv x1) cpsubsp) (cv x2)) (wral (λ x3 . wral (λ x4 . wb (wss (cv x3) (cv x4)) (wss (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)))) (λ x4 . cfv (cv x1) cpsubsp)) (λ x3 . cfv (cv x1) cpsubsp))))) ⟶ wceq cldil (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . crab (λ x3 . wral (λ x4 . wbr (cv x4) (cv x2) (cfv (cv x1) cple) ⟶ wceq (cfv (cv x4) (cv x3)) (cv x4)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x1) claut)))) ⟶ wceq cltrn (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wa (wn (wbr (cv x4) (cv x2) (cfv (cv x1) cple))) (wn (wbr (cv x5) (cv x2) (cfv (cv x1) cple))) ⟶ wceq (co (co (cv x4) (cfv (cv x4) (cv x3)) (cfv (cv x1) cjn)) (cv x2) (cfv (cv x1) cmee)) (co (co (cv x5) (cfv (cv x5) (cv x3)) (cfv (cv x1) cjn)) (cv x2) (cfv (cv x1) cmee))) (λ x5 . cfv (cv x1) catm)) (λ x4 . cfv (cv x1) catm)) (λ x3 . cfv (cv x2) (cfv (cv x1) cldil))))) ⟶ wceq cdilN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) catm) (λ x2 . crab (λ x3 . wral (λ x4 . wss (cv x4) (cfv (cv x2) (cfv (cv x1) cwpointsN)) ⟶ wceq (cfv (cv x4) (cv x3)) (cv x4)) (λ x4 . cfv (cv x1) cpsubsp)) (λ x3 . cfv (cv x1) cpautN)))) ⟶ wceq ctrnN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) catm) (λ x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wceq (cin (co (cv x4) (cfv (cv x4) (cv x3)) (cfv (cv x1) cpadd)) (cfv (csn (cv x2)) (cfv (cv x1) cpolN))) (cin (co (cv x5) (cfv (cv x5) (cv x3)) (cfv (cv x1) cpadd)) (cfv (csn (cv x2)) (cfv (cv x1) cpolN)))) (λ x5 . cfv (cv x2) (cfv (cv x1) cwpointsN))) (λ x4 . cfv (cv x2) (cfv (cv x1) cwpointsN))) (λ x3 . cfv (cv x2) (cfv (cv x1) cdilN))))) ⟶ wceq ctrl (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 . crio (λ x4 . wral (λ x5 . wn (wbr (cv x5) (cv x2) (cfv (cv x1) cple)) ⟶ wceq (cv x4) (co (co (cv x5) (cfv (cv x5) (cv x3)) (cfv (cv x1) cjn)) (cv x2) (cfv (cv x1) cmee))) (λ x5 . cfv (cv x1) catm)) (λ x4 . cfv (cv x1) cbs))))) ⟶ wceq ctgrp (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cpr (cop (cfv cnx cbs) (cfv (cv x2) (cfv (cv x1) cltrn))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . ccom (cv x3) (cv x4))))))) ⟶ wceq ctendo (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cab (λ x3 . w3a (wf (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) cltrn)) (cv x3)) (wral (λ x4 . wral (λ x5 . wceq (cfv (ccom (cv x4) (cv x5)) (cv x3)) (ccom (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)))) (λ x5 . cfv (cv x2) (cfv (cv x1) cltrn))) (λ x4 . cfv (cv x2) (cfv (cv x1) cltrn))) (wral (λ x4 . wbr (cfv (cfv (cv x4) (cv x3)) (cfv (cv x2) (cfv (cv x1) ctrl))) (cfv (cv x4) (cfv (cv x2) (cfv (cv x1) ctrl))) (cfv (cv x1) cple)) (λ x4 . cfv (cv x2) (cfv (cv x1) cltrn))))))) ⟶ wceq cedring_rN (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . ctp (cop (cfv cnx cbs) (cfv (cv x2) (cfv (cv x1) ctendo))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cmpt (λ x5 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x5 . ccom (cfv (cv x5) (cv x3)) (cfv (cv x5) (cv x4)))))) (cop (cfv cnx cmulr) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . ccom (cv x4) (cv x3))))))) ⟶ wceq cedring (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . ctp (cop (cfv cnx cbs) (cfv (cv x2) (cfv (cv x1) ctendo))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cmpt (λ x5 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x5 . ccom (cfv (cv x5) (cv x3)) (cfv (cv x5) (cv x4)))))) (cop (cfv cnx cmulr) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . ccom (cv x3) (cv x4))))))) ⟶ wceq cdveca (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cun (ctp (cop (cfv cnx cbs) (cfv (cv x2) (cfv (cv x1) cltrn))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . ccom (cv x3) (cv x4)))) (cop (cfv cnx csca) (cfv (cv x2) (cfv (cv x1) cedring)))) (csn (cop (cfv cnx cvsca) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x3 x4 . cfv (cv x4) (cv x3)))))))) ⟶ wceq cdia (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cmpt (λ x3 . crab (λ x4 . wbr (cv x4) (cv x2) (cfv (cv x1) cple)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . crab (λ x4 . wbr (cfv (cv x4) (cfv (cv x2) (cfv (cv x1) ctrl))) (cv x3) (cfv (cv x1) cple)) (λ x4 . cfv (cv x2) (cfv (cv x1) cltrn)))))) ⟶ wceq cdvh (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) clh) (λ x2 . cun (ctp (cop (cfv cnx cbs) (cxp (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) ctendo)))) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cxp (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) ctendo))) (λ x3 x4 . cxp (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) ctendo))) (λ x3 x4 . cop (ccom (cfv (cv x3) c1st) (cfv (cv x4) c1st)) (cmpt (λ x5 . cfv (cv x2) (cfv (cv x1) cltrn)) (λ x5 . ccom (cfv (cv x5) (cfv (cv x3) c2nd)) (cfv (cv x5) (cfv (cv x4) c2nd))))))) (cop (cfv cnx csca) (cfv (cv x2) (cfv (cv x1) cedring)))) (csn (cop (cfv cnx cvsca) (cmpt2 (λ x3 x4 . cfv (cv x2) (cfv (cv x1) ctendo)) (λ x3 x4 . cxp (cfv (cv x2) (cfv (cv x1) cltrn)) (cfv (cv x2) (cfv (cv x1) ctendo))) (λ x3 x4 . cop (cfv (cfv (cv x4) c1st) (cv x3)) (ccom (cv x3) (cfv (cv x4) c2nd))))))))) ⟶ x0) ⟶ x0
Theorem df_polarityN : wceq cpolN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) catm)) (λ x1 . cin (cfv (cv x0) catm) (ciin (λ x2 . cv x1) (λ x2 . cfv (cfv (cv x2) (cfv (cv x0) coc)) (cfv (cv x0) cpmap)))))) (proof)
Theorem df_psubclN : wceq cpscN (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wa (wss (cv x1) (cfv (cv x0) catm)) (wceq (cfv (cfv (cv x1) (cfv (cv x0) cpolN)) (cfv (cv x0) cpolN)) (cv x1))))) (proof)
Theorem df_lhyp : wceq clh (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wbr (cv x1) (cfv (cv x0) cp1) (cfv (cv x0) ccvr)) (λ x1 . cfv (cv x0) cbs))) (proof)
Theorem df_laut : wceq claut (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wa (wf1o (cfv (cv x0) cbs) (cfv (cv x0) cbs) (cv x1)) (wral (λ x2 . wral (λ x3 . wb (wbr (cv x2) (cv x3) (cfv (cv x0) cple)) (wbr (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)) (cfv (cv x0) cple))) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) cbs))))) (proof)
Theorem df_watsN : wceq cwpointsN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) catm) (λ x1 . cdif (cfv (cv x0) catm) (cfv (csn (cv x1)) (cfv (cv x0) cpolN))))) (proof)
Theorem df_pautN : wceq cpautN (cmpt (λ x0 . cvv) (λ x0 . cab (λ x1 . wa (wf1o (cfv (cv x0) cpsubsp) (cfv (cv x0) cpsubsp) (cv x1)) (wral (λ x2 . wral (λ x3 . wb (wss (cv x2) (cv x3)) (wss (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)))) (λ x3 . cfv (cv x0) cpsubsp)) (λ x2 . cfv (cv x0) cpsubsp))))) (proof)
Theorem df_ldil : wceq cldil (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . crab (λ x2 . wral (λ x3 . wbr (cv x3) (cv x1) (cfv (cv x0) cple) ⟶ wceq (cfv (cv x3) (cv x2)) (cv x3)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . cfv (cv x0) claut)))) (proof)
Theorem df_ltrn : wceq cltrn (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wa (wn (wbr (cv x3) (cv x1) (cfv (cv x0) cple))) (wn (wbr (cv x4) (cv x1) (cfv (cv x0) cple))) ⟶ wceq (co (co (cv x3) (cfv (cv x3) (cv x2)) (cfv (cv x0) cjn)) (cv x1) (cfv (cv x0) cmee)) (co (co (cv x4) (cfv (cv x4) (cv x2)) (cfv (cv x0) cjn)) (cv x1) (cfv (cv x0) cmee))) (λ x4 . cfv (cv x0) catm)) (λ x3 . cfv (cv x0) catm)) (λ x2 . cfv (cv x1) (cfv (cv x0) cldil))))) (proof)
Theorem df_dilN : wceq cdilN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) catm) (λ x1 . crab (λ x2 . wral (λ x3 . wss (cv x3) (cfv (cv x1) (cfv (cv x0) cwpointsN)) ⟶ wceq (cfv (cv x3) (cv x2)) (cv x3)) (λ x3 . cfv (cv x0) cpsubsp)) (λ x2 . cfv (cv x0) cpautN)))) (proof)
Theorem df_trnN : wceq ctrnN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) catm) (λ x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wceq (cin (co (cv x3) (cfv (cv x3) (cv x2)) (cfv (cv x0) cpadd)) (cfv (csn (cv x1)) (cfv (cv x0) cpolN))) (cin (co (cv x4) (cfv (cv x4) (cv x2)) (cfv (cv x0) cpadd)) (cfv (csn (cv x1)) (cfv (cv x0) cpolN)))) (λ x4 . cfv (cv x1) (cfv (cv x0) cwpointsN))) (λ x3 . cfv (cv x1) (cfv (cv x0) cwpointsN))) (λ x2 . cfv (cv x1) (cfv (cv x0) cdilN))))) (proof)
Theorem df_trl : wceq ctrl (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x2 . crio (λ x3 . wral (λ x4 . wn (wbr (cv x4) (cv x1) (cfv (cv x0) cple)) ⟶ wceq (cv x3) (co (co (cv x4) (cfv (cv x4) (cv x2)) (cfv (cv x0) cjn)) (cv x1) (cfv (cv x0) cmee))) (λ x4 . cfv (cv x0) catm)) (λ x3 . cfv (cv x0) cbs))))) (proof)
Theorem df_tgrp : wceq ctgrp (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cpr (cop (cfv cnx cbs) (cfv (cv x1) (cfv (cv x0) cltrn))) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x2 x3 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x2 x3 . ccom (cv x2) (cv x3))))))) (proof)
Theorem df_tendo : wceq ctendo (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cab (λ x2 . w3a (wf (cfv (cv x1) (cfv (cv x0) cltrn)) (cfv (cv x1) (cfv (cv x0) cltrn)) (cv x2)) (wral (λ x3 . wral (λ x4 . wceq (cfv (ccom (cv x3) (cv x4)) (cv x2)) (ccom (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)))) (λ x4 . cfv (cv x1) (cfv (cv x0) cltrn))) (λ x3 . cfv (cv x1) (cfv (cv x0) cltrn))) (wral (λ x3 . wbr (cfv (cfv (cv x3) (cv x2)) (cfv (cv x1) (cfv (cv x0) ctrl))) (cfv (cv x3) (cfv (cv x1) (cfv (cv x0) ctrl))) (cfv (cv x0) cple)) (λ x3 . cfv (cv x1) (cfv (cv x0) cltrn))))))) (proof)
Theorem df_edring_rN : wceq cedring_rN (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . ctp (cop (cfv cnx cbs) (cfv (cv x1) (cfv (cv x0) ctendo))) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . cmpt (λ x4 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x4 . ccom (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)))))) (cop (cfv cnx cmulr) (cmpt2 (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . ccom (cv x3) (cv x2))))))) (proof)
Theorem df_edring : wceq cedring (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . ctp (cop (cfv cnx cbs) (cfv (cv x1) (cfv (cv x0) ctendo))) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . cmpt (λ x4 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x4 . ccom (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)))))) (cop (cfv cnx cmulr) (cmpt2 (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . ccom (cv x2) (cv x3))))))) (proof)
Theorem df_dveca : wceq cdveca (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cun (ctp (cop (cfv cnx cbs) (cfv (cv x1) (cfv (cv x0) cltrn))) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x2 x3 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x2 x3 . ccom (cv x2) (cv x3)))) (cop (cfv cnx csca) (cfv (cv x1) (cfv (cv x0) cedring)))) (csn (cop (cfv cnx cvsca) (cmpt2 (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x2 x3 . cfv (cv x3) (cv x2)))))))) (proof)
Theorem df_disoa : wceq cdia (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cmpt (λ x2 . crab (λ x3 . wbr (cv x3) (cv x1) (cfv (cv x0) cple)) (λ x3 . cfv (cv x0) cbs)) (λ x2 . crab (λ x3 . wbr (cfv (cv x3) (cfv (cv x1) (cfv (cv x0) ctrl))) (cv x2) (cfv (cv x0) cple)) (λ x3 . cfv (cv x1) (cfv (cv x0) cltrn)))))) (proof)
Theorem df_dvech : wceq cdvh (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) clh) (λ x1 . cun (ctp (cop (cfv cnx cbs) (cxp (cfv (cv x1) (cfv (cv x0) cltrn)) (cfv (cv x1) (cfv (cv x0) ctendo)))) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cxp (cfv (cv x1) (cfv (cv x0) cltrn)) (cfv (cv x1) (cfv (cv x0) ctendo))) (λ x2 x3 . cxp (cfv (cv x1) (cfv (cv x0) cltrn)) (cfv (cv x1) (cfv (cv x0) ctendo))) (λ x2 x3 . cop (ccom (cfv (cv x2) c1st) (cfv (cv x3) c1st)) (cmpt (λ x4 . cfv (cv x1) (cfv (cv x0) cltrn)) (λ x4 . ccom (cfv (cv x4) (cfv (cv x2) c2nd)) (cfv (cv x4) (cfv (cv x3) c2nd))))))) (cop (cfv cnx csca) (cfv (cv x1) (cfv (cv x0) cedring)))) (csn (cop (cfv cnx cvsca) (cmpt2 (λ x2 x3 . cfv (cv x1) (cfv (cv x0) ctendo)) (λ x2 x3 . cxp (cfv (cv x1) (cfv (cv x0) cltrn)) (cfv (cv x1) (cfv (cv x0) ctendo))) (λ x2 x3 . cop (cfv (cfv (cv x3) c1st) (cv x2)) (ccom (cv x2) (cfv (cv x3) c2nd))))))))) (proof)