blob: 02e47a8b48cc283480ab47911703b8c9219a8238 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Lemma match_bool_fn b A B xT xF
: match b as b return forall x : A, B b x with
| true => xT
| false => xF
end
= fun x : A => match b as b return B b x with
| true => xT x
| false => xF x
end.
admit.
Defined.
Lemma match_bool_comm_1 (b : bool) A B (F : forall x : A, B x) t f
: (if b as b return B (if b then t else f) then F t else F f)
= F (if b then t else f).
admit.
Defined.
Hint Rewrite match_bool_fn : matchdb.
Fail Hint Rewrite match_bool_comm_1 : matchdb.
|
