proposition: Lemma checkBad_app : forall ls ls', checkBad ls = true -> checkBad (ls ++ ls') = true.
proof: Proof. induction ls; intuition; simpl in *. apply orb_true_iff in H. intuition. rewrite inRange_app. simpl. trivial. trivial. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF