fact: Fixpoint extend (n:nat) {struct n} : forall w:Set, zn2z w -> word w (S n) := match n return forall w:Set, zn2z w -> word w (S n) with | O => fun w x => x | S m => let aux := extend m in fun w x => WW W0 (aux w x) end.
imports: ZArith Basic_type