defω dup-ℕ : 1.ℕ → [ω.ℕ] =
  λ n ⇒
  case1 n return [ω.ℕ] of {
    zero ⇒ [zero];
    succ _, 1.d ⇒
      case1 d return [ω.ℕ] of { [d] ⇒ [succ d] }
  };

defω plus : 1.ℕ → 1.ℕ → ℕ =
  λ m n ⇒
  case1 m return ℕ of {
    zero        ⇒ n;
    succ _, 1.p ⇒ succ p
  };

defω times-ω : 1.ℕ → ω.ℕ → ℕ =
  λ m n ⇒
  case1 m return ℕ of {
    zero        ⇒ zero;
    succ _, 1.t ⇒ plus n t
  };

defω times : 1.ℕ → 1.ℕ → ℕ =
  λ m n ⇒
  case1 dup-ℕ n return ℕ of {
    [n] ⇒ times-ω m n
  };

defω pred : 1.ℕ → ℕ =
  λ n ⇒
  case1 n return ℕ of { zero ⇒ zero; succ n ⇒ n };

def0 pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
  λ n ⇒ δ i ⇒ n;