fact: Fixpoint reduce_n (n:nat) : word w (S n) -> nT := match n return word w (S n) -> nT with | O => reduce_1n | S m => fun x => match x with | W0 => N0 | WW xh xl => match xh with | W0 => @reduce_n m xl | _ => @c (S m) x end end end.
imports: ZArith Basic_type