proposition: Lemma checkBad_permutation : forall ls1 ls2, Permutation ls1 ls2 -> checkBad ls1 = checkBad ls2.
proof: Proof. induction 1; intuition; simpl in *. rewrite IHPermutation. erewrite inRange_permutation. eauto. trivial. case_eq (eqbBvector b0 b); intuition. apply eqbBvector_sound in H. subst. rewrite eqbBvector_complete. simpl. trivial. case_eq (eqbBvector b b0); intuition. apply eqbBvector_sound in H0. subst. rewrite eqbBvector_complete in H. discriminate. destruct (inRange _ l b0). destruct (inRange _ l b). simpl. trivial. simpl. trivial. simpl. trivial. eauto. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF