fact: Fixpoint str_in_list (s:string)(l:list string) {struct l} : bool := match l with s1::tl => if string_dec s s1 then true else str_in_list s tl | _ => false end.
imports: syntax little denot Bool List String ZArith axiom