Skip to content

Instantly share code, notes, and snippets.

@jozefg

jozefg/one-not-zero.jonprl

Created August 27, 2015 09:21
Show Gist options
  • Save jozefg/4e3368b4374e3a0e73c0 to your computer and use it in GitHub Desktop.
Save jozefg/4e3368b4374e3a0e73c0 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
one-not-zero.jonprl
Operator P : (0).
[P(N)] =def= [natrec(N; unit; _._.void)].
Theorem one-not-zero : [not(=(zero; succ(zero); nat))] {
auto;
assert [P(succ(zero))];
aux {
unfold <P>; hyp-subst ← #1 [h.natrec(h; _; _._._)];
reduce; auto
};
unfold <P>; reduce; auto
}.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment