Use hypotheses when doing compile_match
For the following example:
use list.List constant l: list int = Cons 42 Nil goal G : 42 = match l with Nil -> 0 | Cons x _ -> x end
if I want to get a goal of the form
42 = 42, I must do first
subst_all and only then
compile_match is able to give me
42 = 42.
Would it be possible for
compile_match to use hypotheses of the form
H: e = e' to further simplify goals of the form
match e with e' -> ... end ?