proposition: Lemma inRange_app : forall ls ls' r, inRange ls r = true -> inRange (ls ++ ls') r = true.
proof: Proof. induction ls; intuition; simpl in *. case_eq (eqb r b); intuition. eapply IHls. rewrite H0 in H. trivial. Qed.
imports: Crypto Permutation CompFold Array FCF State