No title

lyxia 2018-03-06 20:08:20.688188 UTC

1Lemma dep_match: forall P b (e1: P true) (e2: P false) (x : P b),
2 match b as y return P y with
3 | true => e1
4 | false => e2
5 end = x ->
6 (exists p : true = b, eq_rect _ P e1 _ p = x) \/
7 (exists p : false = b, eq_rect _ P e2 _ p = x).