proposition: Lemma inRange_in_dec : forall ls r, inRange ls r = if (in_dec (EqDec_dec _) r (map (@snd D R) ls)) then true else false.
proof: Proof. induction ls; intuition; simpl in *. destruct (EqDec_dec R_EqDec b r); subst. rewrite eqb_refl. trivial. case_eq (eqb r b); intuition. rewrite eqb_leibniz in H. subst. intuition. exfalso. intuition. specialize (IHls r). destruct (in_dec (EqDec_dec R_EqDec) r (map (snd (B:=R)) ls)). trivial. trivial. Qed.
imports: Crypto Permutation CompFold Array FCF State