proposition: Theorem arrayLookup_arrayUpdate_None_ne : forall p1 p2 v, p1 <> p2 -> arrayLookup (arrayUpdate None p1 (Some v)) p2 = None.
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