[ O ⇒ λ_.v
| S n' ⇒ λp.op ? (f n' ?) (big_op M n' ? v) ]) (refl ? n).
##[ nrewrite > p; napply le_n
- | #m; #H; napply (f n'); nrewrite > p; napply le_n]
+ | #m; #H; napply (f m); nrewrite > p; napply le_S; nassumption]
nqed.
\ No newline at end of file