proposition: Lemma app_inj' {A} : forall l1 l2 l1' l2' : list A, List.length l1 = List.length l1' -> app l1 l2 = app l1' l2' -> l2 = l2'.
proof: Proof. induction l1; simpl; intros. - destruct l1'; simpl; eauto. simpl in H; discriminate. - destruct l1'; simpl in *; intros. discriminate. injections; 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 Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer Coq.Strings.String Coq.Vectors.Vector Fiat.Narcissus.Formats.WordOpt Fiat.Common.Equality