Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/changing_to_existential.v

Created September 16, 2016 03:01
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mukeshtiwari/0d798aa0d9f8b9d8d873aaefb0796178 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mukeshtiwari/0d798aa0d9f8b9d8d873aaefb0796178 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
changing_to_existential.v
c, d : cand
k : nat
H : Path k c d
============================
Fixpoints.iter (O k) (length (all_pairs cand_all)) Fixpoints.empty_ss (c, d) = true
To
c, d : cand
k : nat
H : Path k c d
============================
exists n, Fixpoints.iter (O k) n Fixpoints.empty_ss (c, d) = true
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment