\defded{variac}{
 \infer{ ° I }{
  \infer{ ° x\to L }{
   \infer{ ° x\to j }{
    \infer{ ° x\to y }{
     s &
     s\to (x\to y) } &
    (x\to y)\to (x\to j) } &
   j\to L } &
  (x\to L)\to I } }
\defded{formacao-com}{
 \infer[\to]{ ° a\to (b\land ©) }{
  a &
  \infer[\land ]{ ° b\land © }{
   b &
   \infer[©]{ ° © }{} } } }
\defded{formacao-sem}{
 \infer{ ° a\to (b\land ©) }{
  a &
  \infer{ ° b\land © }{
   b &
   \infer{ ° © }{} } } }
\defded{formacao-alt}{
 \infer{ ° 3 }{
  1 } }
\defded{demotree}{
 \infer{ ° c }{
  \infer{ ° c }{
   a &
   \infer[R]{ ° b }{
    a } } &
  b &
  \infer[R']{ ° a }{} } }
\defded{demotree-nodes}{
 \infer{ ° n_7 }{
  \infer{ ° n_4 }{
   n_2 &
   \infer{ ° n_3 }{
    n_1 } } &
  n_5 &
  \infer{ ° n_6 }{} } }
\defded{x.g(f(x))}{
 \infer{ ° Ðx.g(f(x)) }{
  \infer{ ° g(f(x)) }{
   \infer{ ° f(x) }{
    x &
    f } &
   g } } }
\defded{x.g(f(x)).t}{
 \infer{ ° a\to c }{
  \infer{ ° c }{
   \infer{ ° b }{
    a &
    a\to b } &
   b\to c } } }
\defded{x.g(f(x)).disch}{
 \infer[1]{ ° Ðx.g(f(x)) }{
  \infer{ ° g(f(x)) }{
   \infer{ ° f(x) }{
    [x]^1 &
    f } &
   g } } }
\defded{x.g(f(x)).disch.t}{
 \infer[1]{ ° a\to c }{
  \infer{ ° c }{
   \infer{ ° b }{
    [a]^1 &
    a\to b } &
   b\to c } } }
\defded{fromtype.1}{
 \infer[2]{ ° Ðx.Ðy.(+)x\,x }{
  \infer[1]{ ° Ðy.(+)x\,x }{
   \infer{ ° (+)x\,x }{
    [x]^2 &
    \infer{ ° (+)x }{
     [x]^2 &
     (+) } } } } }
\defded{fromtype.2}{
 \infer{ ° \nn \to \nn \to \nn  }{
  \infer{ ° \nn \to \nn  }{
   \infer{ ° \nn  }{
    [\nn ]^2 &
    \infer{ ° \nn \to \nn  }{
     [\nn ]^2 &
     \nn \to (\nn \to \nn ) } } } } }
\defded{fromtype.3}{
 \infer[2]{ ° Ð\nn _2.Ð\nn _1.(+)\nn _2\,\nn _2 }{
  \infer[1]{ ° Ð\nn _1.(+)\nn _2\,\nn _2 }{
   \infer{ ° (+)\nn _2\,\nn _2 }{
    [\nn _2]^2 &
    \infer{ ° (+)\nn _2 }{
     [\nn _2]^2 &
     (+) } } } } }
\defded{betared1f}{
 \infer{ ° (Ðx.fx(gx))(hy) }{
  \infer{ ° hy }{
   y &
   h } &
  \infer[1]{ ° Ðx.fx(gx) }{
   \infer{ ° fx(gx) }{
    \infer{ ° gx }{
     [x]^1 &
     g } &
    \infer{ ° fx }{
     [x]^1 &
     f } } } } }
\defded{betared1t}{
 \infer{ ° c }{
  \infer{ ° a }{
   d &
   d\to a } &
  \infer[1]{ ° a\to c }{
   \infer{ ° c }{
    \infer{ ° b }{
     [a]^1 &
     a\to b } &
    \infer{ ° b\to c }{
     [a]^1 &
     a\to (b\to c) } } } } }
\defded{betared2f}{
 \infer{ ° f(hy)(g(hy)) }{
  \infer{ ° g(hy) }{
   \infer{ ° hy }{
    y &
    h } &
   g } &
  \infer{ ° f(hy) }{
   \infer{ ° hy }{
    y &
    h } &
   f } } }
\defded{betared2t}{
 \infer{ ° c }{
  \infer{ ° b }{
   \infer{ ° a }{
    d &
    d\to a } &
   a\to b } &
  \infer{ ° b\to c }{
   \infer{ ° a }{
    d &
    d\to a } &
   a\to (b\to c) } } }
\defded{wideflip.t}{
 \infer[1]{ ° a\land b\to b\land a }{
  \infer{ ° b\land a }{
   \infer{ ° a }{
    [a\land b]^1 &
    \infer{ ° a\land b\to a }{} } &
   \infer{ ° a\to b\land a }{
    \infer{ ° b }{
     [a\land b]^1 &
     \infer{ ° a\land b\to b }{} } &
    \infer{ ° b\to (a\to b\land a) }{} } } } }
\defded{wideflip}{
 \infer[1]{ ° Ðp.\P({\pi_2}p)({\pi_1}p) }{
  \infer{ ° \P({\pi_2}p)({\pi_1}p) }{
   \infer{ ° {\pi_1}p }{
    [p]^1 &
    \infer{ ° {\pi_1} }{} } &
   \infer{ ° \P({\pi_2}p) }{
    \infer{ ° {\pi_2}p }{
     [p]^1 &
     \infer{ ° {\pi_2} }{} } &
    \infer{ ° \P }{} } } } }
\defded{rulef}{
 \infer[\ruleF{C}]{ ° C{\alpha}_1{\alpha}_2\ldots{\alpha}_n }{
  {\alpha}_1 &
  {\alpha}_2 &
  \ldots &
  {\alpha}_n } }
\defded{flip.t}{
 \infer[1]{ ° a\land b\to b\land a }{
  \infer{ ° b\land a }{
   \infer{ ° b }{
    [a\land b]^1 } &
   \infer{ ° a }{
    [a\land b]^1 } } } }
\defded{flip.fr}{
 \infer[1]{ ° Ðp.\P({\pi_2}p)({\pi_1}p) }{
  \infer[\ruleF{\P}]{ ° \P({\pi_2}p)({\pi_1}p) }{
   \infer[\ruleF{{\pi_2}}]{ ° {\pi_2}p }{
    [p]^1 } &
   \infer[\ruleF{{\pi_1}}]{ ° {\pi_1}p }{
    [p]^1 } } } }
\defded{flip.f}{
 \infer[1]{ ° Ðp.\P({\pi_2}p)({\pi_1}p) }{
  \infer{ ° \P({\pi_2}p)({\pi_1}p) }{
   \infer{ ° {\pi_2}p }{
    [p]^1 } &
   \infer{ ° {\pi_1}p }{
    [p]^1 } } } }
\defded{polim1}{
 \infer{ ° \Lambda x.Ðp.Ðf.\cbP({\pi_1}p)(f({\pi_2}p)) }{
  \infer[2]{ ° Ðp.Ðf.\cbP({\pi_1}p)(f({\pi_2}p)) }{
   \infer[1]{ ° Ðf.\cbP({\pi_1}p)(f({\pi_2}p)) }{
    \infer{ ° \cbP({\pi_1}p)(f({\pi_2}p)) }{
     \infer{ ° {\pi_1}p }{
      [p]^2 } &
     \infer{ ° f({\pi_2}p) }{
      \infer{ ° {\pi_2}p }{
       [p]^2 } &
      [f]^1 } } } } } }
\defded{polim2}{
 \infer{ ° x\funto (x\land a\to ((a\to b)\to (x\land b))) }{
  \infer[2]{ ° x\land a\to ((a\to b)\to (x\land b)) }{
   \infer[1]{ ° (a\to b)\to (x\land b) }{
    \infer{ ° x\land b }{
     \infer{ ° x }{
      [x\land a]^2 } &
     \infer{ ° b }{
      \infer{ ° a }{
       [x\land a]^2 } &
      [a\to b]^1 } } } } } }
\defded{bd0}{
 \infer={ ° {\beta} }{
  {\alpha}_1 &
  \ldots &
  {\alpha}_n } }
\defded{bd1}{
 \infer{ ° c }{
  \infer{ ° b }{
   a &
   a\to b } &
  b\to c } }
\defded{bd2}{
 \infer={ ° c }{
  a &
  a\to b &
  b\to c } }
\defded{bd3}{
 \infer[1]{ ° a\to c }{
  \infer{ ° c }{
   \infer{ ° b }{
    [a]^1 &
    a\to b } &
   b\to c } } }
\defded{bd4}{
 \infer[1]{ ° a\to c }{
  \infer={ ° c }{
   [a]^1 &
   a\to b &
   b\to c } } }
\defded{bd5}{
 \infer[1]{ ° a\to c }{
  \infer={ ° c }{
   [a]^1 &
   A } } }
\defded{andI}{
 \infer[\andI]{ ° {\alpha}\land {\beta} }{
  {\alpha} &
  {\beta} } }
\defded{andE1}{
 \infer[\andE1]{ ° {\alpha} }{
  {\alpha}\land {\beta} } }
\defded{andE2}{
 \infer[\andE2]{ ° {\beta} }{
  {\alpha}\land {\beta} } }
\defded{orI1}{
 \infer[\orI1]{ ° {\alpha}\lor {\beta} }{
  {\alpha} } }
\defded{orI2}{
 \infer[\orI2]{ ° {\alpha}\lor {\beta} }{
  {\beta} } }
\defded{orE}{
 \infer[\orE]{ ° {\gamma} }{
  {\alpha}\lor {\beta} &
  \infer={ ° {\gamma} }{
   [{\alpha}] &
   A } &
  \infer={ ° {\gamma} }{
   [{\beta}] &
   B } } }
\defded{toE}{
 \infer[\toE]{ ° {\beta} }{
  {\alpha} &
  {\alpha}\to {\beta} } }
\defded{toI}{
 \infer[\toI]{ ° {\alpha}\to {\beta} }{
  \infer={ ° {\beta} }{
   [{\alpha}] &
   A } } }
\defded{botE}{
 \infer[\botE]{ ° {\alpha} }{
  © } }
\defded{topI}{
 \infer[\topI]{ ° õ }{} }
\defded{orE'}{
 \infer[\orE']{ ° {\gamma} }{
  {\alpha}\lor {\beta} &
  {\alpha}\to {\gamma} &
  {\beta}\to {\gamma} } }
\defded{orE'-tra}{
 \infer[\orE]{ ° {\gamma} }{
  {\alpha}\lor {\beta} &
  \infer{ ° {\gamma} }{
   [{\alpha}] &
   {\alpha}\to {\gamma} } &
  \infer{ ° {\gamma} }{
   [{\beta}] &
   {\beta}\to {\gamma} } } }
\defded{orE-tra}{
 \infer[\orE']{ ° {\gamma} }{
  {\alpha}\lor {\beta} &
  \infer[1]{ ° {\alpha}\to {\gamma} }{
   \infer={ ° {\gamma} }{
    [{\alpha}]^1 &
    A } } &
  \infer[2]{ ° {\beta}\to {\gamma} }{
   \infer={ ° {\gamma} }{
    [{\beta}]^2 &
    B } } } }
\defded{and-norm1}{
 \infer{ ° {\alpha} }{
  \infer{ ° {\alpha}\land {\beta} }{
   \infer={ ° {\alpha} }{
    A } &
   \infer={ ° {\beta} }{
    B } } } }
\defded{and-norm2}{
 \infer={ ° {\alpha} }{
  A } }
\defded{and-norm3}{
 \infer{ ° {\beta} }{
  \infer{ ° {\alpha}\land {\beta} }{
   \infer={ ° {\alpha} }{
    A } &
   \infer={ ° {\beta} }{
    B } } } }
\defded{and-norm4}{
 \infer={ ° {\beta} }{
  B } }
\defded{to-norm1}{
 \infer{ ° {\beta} }{
  \infer={ ° {\alpha} }{
   A } &
  \infer[1]{ ° {\alpha}\to {\beta} }{
   \infer={ ° {\beta} }{
    [{\alpha}]^1 &
    B } } } }
\defded{to-norm2}{
 \infer={ ° {\beta} }{
  \infer={ ° {\alpha} }{
   A } &
  B } }
\defded{or-norm1}{
 \infer[1]{ ° {\gamma} }{
  \infer{ ° {\alpha}\lor {\beta} }{
   \infer={ ° {\alpha} }{
    A' } } &
  \infer={ ° {\gamma} }{
   [{\alpha}]^1 &
   A } &
  \infer={ ° {\gamma} }{
   [{\beta}]^1 &
   B } } }
\defded{or-norm2}{
 \infer={ ° {\gamma} }{
  \infer={ ° {\alpha} }{
   A' } &
  A } }
\defded{or-norm3}{
 \infer[1]{ ° {\gamma} }{
  \infer{ ° {\alpha}\lor {\beta} }{
   \infer={ ° {\beta} }{
    B' } } &
  \infer={ ° {\gamma} }{
   [{\alpha}]^1 &
   A } &
  \infer={ ° {\gamma} }{
   [{\beta}]^1 &
   B } } }
\defded{or-norm4}{
 \infer={ ° {\gamma} }{
  \infer={ ° {\beta} }{
   B' } &
  B } }
\defded{cpex1}{
 \infer{ ° a }{
  \infer{ ° a\land c }{
   a\lor ªb &
   \infer{ ° a\land c }{
    [a]^1 &
    c } &
   \infer{ ° a\land c }{
    \infer{ ° © }{
     b &
     [ªb]^1 } } } } }
\defded{cpex2}{
 \infer[1]{ ° a }{
  a\lor ªb &
  \infer{ ° a }{
   \infer{ ° a\land c }{
    [a]^1 &
    c } } &
  \infer{ ° a }{
   \infer{ ° a\land c }{
    \infer{ ° © }{
     b &
     [ªb]^1 } } } } }
\defded{cpex3}{
 \infer[1]{ ° a }{
  a\lor ªb &
  [a]^1 &
  \infer{ ° a }{
   \infer{ ° a\land c }{
    \infer{ ° © }{
     b &
     [ªb]^1 } } } } }
\defded{cpex4}{
 \infer[1]{ ° a }{
  a\lor ªb &
  [a]^1 &
  \infer{ ° a }{
   \infer{ ° © }{
    b &
    [ªb]^1 } } } }
\defded{ExE}{
 \infer[1:\ExE]{ ° õ_\phi }{
  õ_{íx} &
  \infer={ ° õ_\phi }{
   [x]^1 &
   A } } }
\defded{ExI}{
 \infer[\ExI]{ ° õ_{íx.\phi} }{
  x &
  õ_\phi } }
\defded{FaE}{
 \infer[\FaE]{ ° õ_\phi }{
  x &
  õ_{ìx.\phi} } }
\defded{FaI}{
 \infer[1:\FaI]{ ° õ_{ìx.\phi} }{
  \infer={ ° õ_\phi }{
   [x]^1 &
   A } } }
\defded{praw19.1}{
 \infer[\ExI]{ ° õ_{íy.(Pxy\land Pyx)} }{
  y &
  \infer{ ° õ_{Pxy\land Pyx} }{
   õ_{Pxy} &
   \infer{ ° õ_{Pyx} }{
    õ_{Pxy} &
    \infer[\FaE]{ ° õ_{(Pxy\to Pyx)} }{
     y &
     \infer[\FaE]{ ° õ_{ìx.(Pxy\to Pyx)} }{
      x &
      õ_{ìx.ìy.(Pxy\to Pyx)} } } } } } }
\defded{praw19.2}{
 \infer[2:\FaI]{ ° õ_{ìx.íy.(Pxy\land Pyx)} }{
  \infer[1:\ExE]{ ° õ_{íy.(Pxy\land Pyx)} }{
   \infer[\FaE]{ ° õ_{íy.Pxy} }{
    [x]^2 &
    õ_{ìx.íy.Pxy} } &
   \infer={ ° õ_{íy.(Pxy\land Pyx)} }{
    [x]^2 &
    \infer{ ° y }{
     [y|_{Pxy}]^1 } &
    \infer{ ° õ_{Pxy} }{
     [y|_{Pxy}]^1 } &
    õ_{ìx.ìy.(Pxy\to Pyx)} } } } }
\defded{praw19-orig1}{
 \infer[\FaI]{ ° ìx.íy.(Pxy\land Pyx) }{
  \infer[1:\ExE]{ ° íy.(Pay\land Pya) }{
   \infer[\FaE]{ ° íy.Pay }{
    ìx.íy.Pxy } &
   \infer[\ExI]{ ° íy.(Pay\land Pya) }{
    \infer{ ° Pab\land Pba }{
     [Pab]^1 &
     \infer{ ° Pba }{
      [Pab]^1 &
      \infer[\FaE]{ ° Pab\to Pba }{
       \infer[\FaE]{ ° ìy.(Pay\to Pya) }{
        ìx.ìy.(Pxy\to Pyx) } } } } } } } }
\defded{praw19-orig2}{
 \infer[\FaI]{ ° ìx.íy.(Pxy\land Pyx) }{
  \infer[1:\ExE]{ ° íy.(Pxy\land Pyx) }{
   \infer[\FaE]{ ° íy.Pxy }{
    ìx.íy.Pxy } &
   \infer[\ExI]{ ° íy.(Pxy\land Pyx) }{
    \infer{ ° Pxy\land Pyx }{
     [Pxy]^1 &
     \infer{ ° Pyx }{
      [Pxy]^1 &
      \infer[\FaE]{ ° Pxy\to Pyx }{
       \infer[\FaE]{ ° ìy.(Pxy\to Pyx) }{
        ìx.ìy.(Pxy\to Pyx) } } } } } } } }
\defded{admiss-ExE}{
 \infer[1:\ExE]{ ° õ_{\gamma} }{
  õ_{í{\alpha}} &
  \infer={ ° õ_{\gamma} }{
   [{\alpha}]^1 &
   {\beta} } } }
\defded{crdom}{
 \infer{ ° \O_{\alpha} }{
  {\alpha}\to {\beta} } }
\defded{crcod}{
 \infer{ ° \O_{\beta} }{
  {\alpha}\to {\beta} } }
\defded{crcomp}{
 \infer{ ° {\alpha}\to {\gamma} }{
  {\alpha}\to {\beta} &
  {\beta}\to {\gamma} } }
\defded{crid}{
 \infer{ ° {\alpha}\to {\alpha} }{
  \O_{\alpha} } }
\defded{constrboba1}{
 \infer{ ° a\to b }{
  a\ton{f}b &
  \infer{ ° b\to b }{
   \infer{ ° \O_b }{
    a\ton{f}b } } } }
\defded{cnex1}{
 \infer{ ° a\to a' }{
  a\ton{f}c &
  c\to a' } }
\defded{cnex2}{
 \infer{ ° a\to a' }{
  a\ton{g}c &
  c\to a' } }
\defded{cnex3}{
 a\ton{\id}a' }
\defded{cnex4}{
 \infer{ ° a\to a' }{
  a\to b &
  b\to a' } }
\defded{cn-withpoints}{
 \infer[1]{ ° a\to a' }{
  \infer{ ° a' }{
   \infer{ ° c }{
    [a]^1 &
    a\ton{f}c } &
   c\to a' } } }
\defded{comp1}{
 \infer[½]{ ° a\to c }{
  a\to b &
  b\to c } }
\defded{comp2}{
 \infer{ ° a\ton{g½f}c }{
  a\ton{f}b &
  b\ton{g}c } }
\defded{comp3}{
 \infer{ ° a\ton{f}b\ton{g}c }{
  a\ton{f}b &
  b\ton{g}c } }
\defded{comp4}{
 \infer{ ° a\to b\to c }{
  a\to b &
  b\to c } }
\defded{comp5}{
 \infer[½]{ ° g½f }{
  f &
  g } }
\defded{comp0a}{
 \infer{ ° a\to c }{
  a\to b &
  b\to c } }
\defded{comp0b}{
 \infer{ ° g½f }{
  f &
  g } }
\defded{functor0.a}{
 \infer{ ° a^F\to c^F }{
  \infer{ ° a^F\to b^F }{
   a\to b } &
  \infer{ ° b^F\to c^F }{
   b\to c } } }
\defded{functor0.b}{
 \infer{ ° a^F\to c^F }{
  \infer{ ° a\to c }{
   a\to b &
   b\to c } } }
\defded{functor0.af}{
 \infer{ ° f^F½g^F }{
  \infer{ ° g^F }{
   g } &
  \infer{ ° f^F }{
   f } } }
\defded{functor0.bf}{
 \infer{ ° (f½g)^F }{
  \infer{ ° f½g }{
   g &
   f } } }
\defded{functor-exp}{
 \infer[2]{ ° (i\to a)\to (i\to b) }{
  \infer[1]{ ° i\to b }{
   \infer{ ° b }{
    \infer{ ° a }{
     [i]^1 &
     [i\to a]^2 } &
    a\to b } } } }
\defded{tn1}{
 \infer[\mathrm{TN}]{ ° {\alpha}^{FH}\to {\alpha}^{FK} }{
  \infer[F]{ ° \O_{{\alpha}^F} }{
   \O_{\alpha} } } }
\defded{tn2}{
 \infer[H]{ ° {\alpha}^{FH}\to {\alpha}^{GH} }{
  \infer[\mathrm{TN}]{ ° {\alpha}^F\to {\alpha}^G }{
   \O_{\alpha} } } }
\defded{prod1}{
 \infer{ ° x\to p }{
  x\to a &
  x\to b &
  \coneab{p} } }
\defded{prod2}{
 \infer[ž]{ ° {\alpha}\to {\beta}\land {\gamma} }{
  {\alpha}\to {\beta} &
  {\alpha}\to {\gamma} } }
\defded{prod2p1}{
 \infer[\pi]{ ° {\beta}\land {\gamma}\to {\beta} }{} }
\defded{prod2p2}{
 \infer[\pi']{ ° {\beta}\land {\gamma}\to {\gamma} }{} }
\defded{prodeq1a}{
 \infer{ ° {\alpha}\to {\beta} }{
  \infer{ ° {\alpha}\to {\beta}\land {\gamma} }{
   {\alpha}\to {\beta} &
   {\alpha}\to {\gamma} } &
  \infer{ ° {\beta}\land {\gamma}\to {\beta} }{} } }
\defded{prodeq1b}{
 {\alpha}\to {\beta} }
\defded{prodeq2a}{
 \infer{ ° {\alpha}\to {\gamma} }{
  \infer{ ° {\alpha}\to {\beta}\land {\gamma} }{
   {\alpha}\to {\beta} &
   {\alpha}\to {\gamma} } &
  \infer{ ° {\beta}\land {\gamma}\to {\gamma} }{} } }
\defded{prodeq2b}{
 {\alpha}\to {\gamma} }
\defded{prodeq3a}{
 \infer{ ° {\alpha}\to {\beta}\land {\gamma} }{
  \infer={ ° {\alpha}\to {\beta} }{
   {\alpha}\to {\beta}\land {\gamma} } &
  \infer={ ° {\alpha}\to {\gamma} }{
   {\alpha}\to {\beta}\land {\gamma} } } }
\defded{prodeq3b}{
 {\alpha}\to {\beta}\land {\gamma} }
\defded{functor-prod}{
 \infer{ ° {\alpha}\land c\to {\beta}\land c }{
  \infer{ ° {\alpha}\land c\to {\beta} }{
   \infer{ ° {\alpha}\land c\to {\alpha} }{} &
   {\alpha}\to {\beta} } &
  \infer{ ° {\alpha}\land c\to c }{} } }
\defded{adj-abc1}{
 \infer{ ° a^R\to c }{
  \infer{ ° a\to c^L }{
   a\to b &
   b\to c^L } } }
\defded{adj-abc2}{
 \infer{ ° a^R\to c }{
  \infer{ ° a^R\to b^R }{
   a\to b } &
  b^R\to c } }
\defded{adj-bcd1}{
 \infer{ ° b\to d^L }{
  \infer{ ° b^R\to d }{
   b^R\to c &
   c\to d } } }
\defded{adj-bcd2}{
 \infer{ ° b\to d^L }{
  b\to c^L &
  \infer{ ° c^L\to d^L }{
   c\to d } } }
\defded{adj-bijdown}{
 \infer{ ° a\to b^L }{
  a\to a^{RL} &
  \infer{ ° a^{RL}\to b^L }{
   a^R\to b } } }
\defded{adj-bijup}{
 \infer{ ° a^R\to b }{
  a\to b^L } }
\defded{adj-functor}{
 \infer{ ° a^R\to b^R }{
  \infer{ ° a\to b^{RL} }{
   a\to b &
   \infer{ ° b\to b^{RL} }{
    \infer{ ° \O_b }{
     a\to b } } } } }
\defded{CCCid}{
 \infer[\id]{ ° {\alpha}\to {\alpha} }{} }
\defded{CCCcomp}{
 \infer[½]{ ° {\alpha}\to {\gamma} }{
  {\alpha}\to {\beta} &
  {\beta}\to {\gamma} } }
\defded{CCCandI}{
 \infer[\andI_\CCC]{ ° {\alpha}\to {\beta}\land {\gamma} }{
  {\alpha}\to {\beta} &
  {\alpha}\to {\gamma} } }
\defded{CCCpi1}{
 \infer[\pi]{ ° {\alpha}\land {\beta}\to {\alpha} }{} }
\defded{CCCpi2}{
 \infer[\pi']{ ° {\alpha}\land {\beta}\to {\beta} }{} }
\defded{CCCorI}{
 \infer[\orI\CCC]{ ° {\alpha}\lor {\beta}\to {\gamma} }{
  {\alpha}\to {\gamma} &
  {\beta}\to {\gamma} } }
\defded{CCCk1}{
 \infer[\kappa]{ ° {\alpha}\to {\alpha}\lor {\beta} }{} }
\defded{CCCk2}{
 \infer[\kappa']{ ° {\beta}\to {\alpha}\lor {\beta} }{} }
\defded{CCCcur}{
 \infer[\cur]{ ° {\alpha}\to ({\beta}\to {\gamma}) }{
  {\alpha}\land {\beta}\to {\gamma} } }
\defded{CCCev}{
 \infer[\ev]{ ° {\alpha}\land ({\alpha}\to {\beta})\to {\beta} }{} }
\defded{CCCT}{
 \infer[õ_\CCC]{ ° {\alpha}\to õ }{} }
\defded{CCCbot}{
 \infer[©_\CCC]{ ° ©\to {\alpha} }{} }
\defded{uncur}{
 \infer{ ° {\alpha}\land {\beta}\to {\gamma} }{
  \infer{ ° {\alpha}\land {\beta}\to {\beta}\land ({\beta}\to {\gamma}) }{
   \infer{ ° {\alpha}\land {\beta}\to {\beta} }{} &
   \infer{ ° {\alpha}\land {\beta}\to ({\beta}\to {\gamma}) }{
    \infer{ ° {\alpha}\land {\beta}\to {\alpha} }{} &
    {\alpha}\to ({\beta}\to {\gamma}) } } &
  \infer{ ° {\beta}\land ({\beta}\to {\gamma})\to {\gamma} }{} } }
\defded{bijs-2pbs}{
 \infer{ ° x\to a }{
  \infer{ ° x\to (a,c,b,d,e,f) }{
   \infer[*]{ ° x\to (c,b,d,e,f) }{
    \infer{ ° x\to (c,d,e,f) }{
     \infer{ ° x\to (c,d,f) }{
      x\to a' } } } } } }
\endinput