proposition: Theorem arrayLookup_app_None : forall (A B : Set)(eqd : EqDec A)(ls1 ls2 : list (A * B))(a : A), arrayLookup eqd ls1 a = None -> arrayLookup eqd (ls1 ++ ls2) a = arrayLookup eqd ls2 a.
proof: Proof. induction ls1; intuition; simpl in *. case_eq (eqb a a0); intuition; rewrite H0 in H. discriminate. eauto. Qed.
imports: FCF.Crypto FCF.Fold Permutation FCF.CompFold