proposition: Theorem arrayLookup_arrayUpdate_eq : forall arr p v, arrayLookup (arrayUpdate arr p (Some v)) p = (Some v).
proof: Proof. intuition. unfold arrayUpdate. destruct arr. simpl. rewrite eqb_refl. trivial. simpl. rewrite eqb_refl. trivial. Qed.
imports: FCF.Crypto FCF.Fold Permutation