Skip to content

Instantly share code, notes, and snippets.

@siddhartha-gadgil

siddhartha-gadgil/ThemConstFn.agda

Created March 25, 2014 06:04
Show Gist options
  • Save siddhartha-gadgil/9756012 to your computer and use it in GitHub Desktop.
Save siddhartha-gadgil/9756012 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ThemConstFn.agda
open import Nat
-- If f(m+1) = f(m) for all m, then f(n) = f(0) for all n
constthm : (f : ℕ → ℕ) → ((m : ℕ) → (f (succ m)) == (f m)) → (n : ℕ) → (f n) == (f 0)
constthm f _ 0 = refl (f 0)
constthm f adjEq (succ n) = (adjEq n) transEq (constthm f adjEq n)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment