#include "../prelude/logic.ncc"

-- just because we can define the theorem 
-- doesn't mean we can prove it (we don't have switch?)

defn natural : prop
  as ∀ a : prop . a → (a → a)  → a

defn zero : natural
  as λ a : prop . λ z : a . λ s : a → a . z

defn succ : natural → natural
  as λ n : natural . λ a : prop . λ z : a . λ s : a → a . s (n a z s)

defn even : natural → prop
   | even-zero = even zero
   | even-succ = [A : natural] even A -> even (succ (succ A))

defn add : natural → natural → natural
  as λ n₁ n₂ : natural . n₁ natural n₂ succ

defn thm : prop
  as ∀ N . even (add N N)