proposition: Lemma inRange_permutation : forall ls1 ls2 r, Permutation ls1 ls2 -> inRange ls1 r = inRange ls2 r.
proof: Proof. induction 1; intuition; simpl in *. rewrite IHPermutation. trivial. case_eq (eqb r b0); intuition. rewrite eqb_leibniz in H. subst. destruct (eqb b0 b); intuition. eauto. Qed.
imports: Crypto Permutation CompFold Array FCF State