proposition: Theorem arrayLookup_arrayUpdate_ne : forall arr p1 p2 v, p1 <> p2 -> arrayLookup (arrayUpdate (Some arr) p1 (Some v)) p2 = arrayLookup arr p2.
proof: Proof. intuition. unfold arrayUpdate. simpl. case_eq (eqb p2 p1); intuition. rewrite eqb_leibniz in H0. subst. intuition. Qed.
imports: FCF.Crypto FCF.Fold Permutation