gistfile1.txt

Theorem foo : ⸤⊢ (n:nat) =(zero; succ(n); nat) -> =(zero; succ(n); nat)⸥ {
  fun-intro(n.fun-intro(x.x; eq⁼(nat-eq; zero-eq; succ-eq(hyp-eq(n)))); nat-eq)
} ext {
  lam(_.lam(x.x))
}.

Operator is-zero : (0).
⸤is-zero(n)⸥ ≝ ⸤natrec(n; unit; _._.void)⸥.

Theorem succ-not-zero : ⸤⊢ (n:nat) =(succ(n); zero; nat) -> void⸥ {
  fun-intro(n.fun-intro(x.assert(subst(x; ~<=-refl; h.natrec-eq(hyp-eq(h); ~<=-eq(base-member-eq(~-~<=(~<=-refl; ~<=-refl)); base-member-eq(~-~<=(~<=-refl; ~<=-refl))); _._.~<=-eq(base-member-eq(~-~<=(~<=-refl; ~<=-refl)); base-member-eq(~-~<=(~<=-refl; ~<=-refl))))); H.assert(H; h.assert(~-subst(~-~<=(assume-has-value(v.bottom-div(v); ~<=-eq(base-member-eq(~-~<=(~<=-refl; ~<=-refl)); base-member-eq(~-~<=(~<=-refl; ~<=-refl)))); h); ~<=-refl); q.bottom-div(q)))); eq⁼(nat-eq; succ-eq(hyp-eq(n)); zero-eq)); nat-eq)
} ext {
  lam(_.lam(_.<>))
}.