fact: Definition arrayUpdate (arr_opt : option Array) d r_opt := let arr := match arr_opt with | None => nil | Some arr => arr end in match r_opt with | None => arr | Some r => (d, r) :: arr end.
imports: FCF.Crypto FCF.Fold Permutation