Skip to content

Instantly share code, notes, and snippets.

@wilcoxjay

wilcoxjay/vanila.v

Created August 31, 2015 15:35
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save wilcoxjay/c98e6bb39847bce69065 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
vanila.v
Require Import Arith.
Section vanila.
Variable A B : Type.
Variable lift : nat -> B -> A.
Variable u v n : nat.
Variable var : nat -> B.
Variable a : A.
Goal lift (S u) (if le_gt_dec v n then var (S n) else var n) = a.
match goal with
| [ |- context [ le_gt_dec ?x ?y ] ] => destruct (le_gt_dec x y)
end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment