Since you don't provide your code, I will not try to make sure this works, but the gist of it is to do a dependent inversion, passing the type that should be used:
dependent inversion test with (
fun t v =>
match t as _t return val _t -> Prop with
| Bool => fun v => eval (If v b1 b2) = eval b1 \/ eval (If v b1 b2) = eval b2
| _ => fun v => False
end v
).
This is basically equivalent to writing your own dependent pattern matching in such a way that the thing in the with
clause up there is your return annotation.
It is somewhat equivalent to doing that:
refine (
match test as _test in val _t return
match _t as __t return val __t -> Prop with
| Bool => fun test => eval (If test b1 b2) = eval b1 \/ eval (If test b1 b2) = eval b2
| _ => fun _ => _t = Bool -> False
end _test
with
| T => _
| F => _
| _ => _
end
); try discriminate.