After playing with the Program
command I managed to build a refine that might suites you, but I don't understand everything I did. The main idea is to help Coq with the substitution by introducing intermediate equalities that will serve as brige within the substitution
refine ((fun fl =>
match fl as fl0 return (fl0 = fl -> fail_hard_omat fl0 = 0) with
| mkFail n bar =>
match n as n0 return (forall foo: (forall x:nat, x < n0 -> nat),
mkFail n0 foo = fl -> fail_hard_omat (mkFail n0 foo) = 0) with
| O => _
| S p => _
end bar
end (eq_refl fl) ) fl).
Anyway, I don't know what your purpose here is, but I advise never write dependent match "by hand" and rely on Coq's tactics. In your case, if you define your Definition failomat
with Defined.
instead of Qed
, you will be able to unfold it and you won't need dependent matching.
Hope it helps, V.
Note: both occurences of bar
can be replaced by an underscore.