The Coq mailing list

[Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>]

Thanks for the interesting "Repeat Constructor", that I didn't know.
It does not help in avoiding the evaluation of accessibility arguments,
but at least it saves much time.

Your trick is usable even if more than one constructor can be applied.
In my example I can replace 
  Definition ok124 := Eval Lazy... in (all_acc_div2 (124)).
with
  Definition ok124 : (acc_div2 (124)).
  Repeat Constructor.
  Defined.

Note also that your program has a completely different computational meaning 
since your fAcc has type nat -> Set, instead of nat -> Prop.
(this is related to the remarks of Randy).

Best,
  Jean-Francois