proposition: Lemma inRange_map : forall ls x, inRange ls x = true -> In x (map (@snd D R) ls).
proof: Proof. induction ls; intuition; simpl in *. discriminate. case_eq (eqb x b); intuition. rewrite eqb_leibniz in H0. subst. intuition. right. eapply IHls. rewrite H0 in H. trivial. Qed.
imports: Crypto Permutation CompFold Array FCF State