proposition: Lemma split_BitString_inj : forall l l', split_BitString l = split_BitString l' -> l = l'.
proof: Proof. intro; generalize (le_refl (length l)); remember (length l). rewrite Heqn at 1; clear Heqn; revert l; induction n. - destruct l; simpl; intros. destruct l'; simpl in *; eauto. destruct l' as [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? ] ] ] ] ] ] ]; try (simpl; intros; congruence). destruct (split_BitString l); simpl; intros; discriminate. inversion H. - intros l H; destruct l as [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? ] ] ] ] ] ] ] ]; try (simpl; intros; congruence); destruct l' as [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? [ | ? ] ] ] ] ] ] ] ]; try (simpl; intros; first [discriminate | congruence | injection H0; congruence | destruct (split_BitString l); congruence]). simpl; intros. destruct (split_BitString l) eqn : ? ; destruct (split_BitString l0) eqn : ? . injections; repeat f_equal. eapply IHn; simpl in H; try omega. congruence. 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