integer-addition-with-proof.jmda

{ =: [A: Type, a: A, b: A :: Type],
    refl: [A: Type, a: A :: (= a a)],
  (. dependent pair .)
  DPair: [A: Type, B: [_: A :: Type] :: Type],
    dpair: [A: Type, B: [_: A :: Type], a: A, b: (B a) :: (DPair A (B a))],
    dfst: [A: Type, a: A, B: [_: A :: Type], pr: (DPair A (B a)) :: A],
    dsnd: [A: Type, a: A, B: [_: A :: Type], pr: (DPair A (B a)) :: (B a)],
  Int: Type,
    0: Int,
    s: [_: Int :: Int],
    match: [value: Int, R: Type, 0f: R, sf: [n: Int :: R] :: R],
    p_match_0: [R: Type, 0f: R, sf: [n: Int :: R] :: (= R 0f (match 0 R 0f sf))]
    p_match_s: [R: Type, 0f: R, sf: [n: Int :: R], n: Int :: (= R (sf n) (match (s n) R 0f sf))]
  :: (DPair
    [x: Int, y: Int :: Int]
    { add: [x: Int, y: Int :: Int] :: Type . (= Int y (add 0 y)) }
  .
  let Add = [x: Int, y: Int :: Int] .
  let add = { x: Int, y: Int :: Int as add.
    (match x Int y { n: Int :: Int . (add n (s y)) })
  }.
  (dpair Add { add: Add :: Type . (= Int y (add 0 y)) }
    add
    (p_match_0 Int y (add 0 y))
  )
}