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