fact: Fixpoint lookup {A: Type} (x: string) (l: list (string * A)) : option A := match l with | nil => None | (y, a) :: l => if string_dec x y then Some a else lookup x l end.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)