Disjointness of constructors in Pie

Question

Is it possible to get a proof of the disjointness of constructors in Pie?

For example, is there a term of type (Pi ((n Nat)) (-> (= Nat (add1 n) 0)) Absurd))?

Answer 1

Answered by mietek on ##dependent on Freenode:

(claim disjoint-Nat (Pi ((n Nat)) (-> (= Nat (add1 n) 0) Absurd)))
(define disjoint-Nat
  (lambda (n prf)
    (replace
      prf
      (lambda (n) (iter-Nat n Absurd (lambda (_) Trivial)))
      sole)))