File "./htt/array.v", line 151, characters 0-59:
Error:
In nested Ltac calls to "by (ssrhintarg)" and "done", last call failed.
No applicable tactic.
If I remove by on that line, the proof state is:
1 subgoal
I : finType
T : Type
a : {array I -> T}
f : {ffun I -> T}
V : valid (updi a (fgraph f))
______________________________________(1/1)
[/\ updi a [seq f i | i <- enum I] = updi a [seq f i | i <- enum I], true & #|I| + 0 = #|I|]
The error is
If I remove
by
on that line, the proof state is: