proposition: Lemma funcLookup_inRange_true : forall s d r, s#d = Some r -> inRange s r = true.
proof: Proof. induction s; intuition; simpl in *. discriminate. case_eq (eqb d a0); intuition; rewrite H0 in H. inversion H; clear H; subst. rewrite eqb_refl. trivial. case_eq (eqb r b); intuition. eauto. Qed.
imports: Crypto Permutation CompFold Array FCF State