Skip to content

Instantly share code, notes, and snippets.

@wilcoxjay

wilcoxjay/necessity.v

Created October 12, 2015 22:02
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save wilcoxjay/5dad794e8be8918be8bb to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save wilcoxjay/5dad794e8be8918be8bb to your computer and use it in GitHub Desktop.
Download ZIP
Raw
necessity.v
Theorem necessity :
forall T (f : T -> nat -> T),
(forall b t, fold b f t = fold' b f t) ->
(forall b n1 n2, f (f b n1) n2 = f (f b n2) n1).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment