type Term
  = (Lam bod)
  | (App fun arg)
  | (Sup lab fst snd)
  | (Dup lab val bod)
  | (Var idx)

#  (λx(bod) arg)
#  ------------- APP-LAM
#  x <- arg
#  bod
(APP (Term/Lam bod) arg) =
  (bod arg)

#  (#i{g,h} arg)
#  ----------------- APP-SUP
#  dup #i{a,b} = arg
#  #i{(g a) (h b)}
(APP (Term/Sup i g h) arg) =
  (DUP i arg λaλb
  (Term/Sup i (APP g a) (APP h b)))

#  ((dup #i{x,y} = val; bod) arg)
#  ------------------------------ APP-DUP
#  (dup #i{x,y} = val; (bod arg))
(APP (Term/Dup i val bod) arg) =
  (DUP i val λaλb(APP (bod a b) arg))

#  (fun arg)
#  --------- APP
#  (fun arg)
(APP fun arg) =
  (Term/App fun arg)

#  dup #i{k0,k1} = λx(f); bod
#  -------------------------- DUP-LAM
#  dup #i{f0,f1} = f
#  x  <- #i{x0,x1}
#  k0 <- λx0(f0)
#  k1 <- λx1(f1)
#  bod
(DUP i (Term/Lam f) bod) =
  (DUP i (f (Term/Sup i $x0 $x1)) λf0λf1
  (bod (Term/Lam λ$x0(f0)) (Term/Lam λ$x1(f1))))

#  dup #i{k0,k1} = #j{fst,snd}; bod
#  -------------------------------- DUP-SUP
#  if #i == #j:
#    k0 <- fst
#    k1 <- snd
#    bod
#  else:
#    k0 <- #j{a0,b0}
#    k1 <- #j{a1,b1}
#    dup #i{a0,a1} = fst
#    dup #i{b0,b1} = snd
#    cont
(DUP i (Term/Sup j fst snd) bod) =
  switch (== i j) {
    0:
      (DUP i fst λa0λa1
      (DUP i snd λb0λb1
      (bod
        (Term/Sup j a0 b0)
        (Term/Sup j a1 b1))))
    _:
      (bod fst snd)
  }

#  dup #i{k0,k1} = (dup #j{r0,r1} = v; f); bod
#  ------------------------------------------- DUP-DUP
#  dup #j{r0,r1} = v
#  dup #i{k0,k1} = f
#  bod
(DUP i (Term/Dup j v f) bod) =
  (DUP j v λr0λr1
  (DUP i (f r0 r1) bod))

#  dup #i{k0,k1} = val; bod
#  ---------------------- DUP
#  dup #i{k0,k1} = val; bod
(DUP i val bod) =
  (Term/Dup i val bod)

(Quote (Term/Lam bod)         dep) = (Term/Lam λx(Quote (bod (Term/Var dep)) (+ dep 1)))
(Quote (Term/App fun arg)     dep) = (Term/App (Quote fun dep) (Quote arg dep))
(Quote (Term/Sup lab fst snd) dep) = (Term/Sup lab (Quote fst dep) (Quote snd dep))
(Quote (Term/Dup lab val bod) dep) = (Term/Dup lab (Quote val dep) λx0λx1(Quote (bod (Term/Var dep) (Term/Var (+ dep 1))) (+ dep 2)))
(Quote (Term/Var idx)         dep) = (Term/Var idx)

C2a = (Term/Lam λf(Term/Lam λx(DUP 0 f λf0λf1(APP f0 (APP f1 x)))))
C2b = (Term/Lam λf(Term/Lam λx(DUP 1 f λf0λf1(APP f0 (APP f1 x)))))
Not = (Term/Lam λb(Term/Lam λt(Term/Lam λf(APP (APP b f) t))))

Main = (Quote (APP C2a C2b) 0)