Skip to content

Instantly share code, notes, and snippets.

@jad-hamza

jad-hamza/dep_match.v

Created March 6, 2018 07:32
Show Gist options
  • Save jad-hamza/d7a4d210f0ad380f4257b28793a9f075 to your computer and use it in GitHub Desktop.
Save jad-hamza/d7a4d210f0ad380f4257b28793a9f075 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
dep_match.v
Lemma dep_match: forall P b (e1: P true) (e2: P false) x,
match b as y return P y with
| true => e1
| false => e2
end = x ->
(b = true /\ e1 = x) \/
(b = false /\ e2 = x).
Admitted.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment