proposition: Lemma inRange_app_cons : forall ls d r x, inRange (ls ++ (d, r) :: nil) x = inRange ((d , r) :: ls) x.
proof: Proof. intuition. symmetry. eapply inRange_permutation. eapply Permutation_cons_append. Qed.
imports: Crypto Permutation CompFold Array FCF State