proposition: Lemma append_word_assoc {n m p} : forall w w' w'', append_word w (append_word w' w'') = eq_rect _ _ (append_word (append_word w w') w'') _ (eq_sym (plus_assoc' n m p)).
proof: Proof. induction w; simpl; intros. - reflexivity. - rewrite IHw; clear. rewrite succ_eq_rect. f_equal. apply eq_proofs_unicity; intros. destruct (eq_nat_dec x y); eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs