fact: Fixpoint mem (k : key) (s : farray) {struct s} : bool := match s with | nil => false | (k',_) :: l => match compare k k' with | LT _ => false | EQ _ => true | GT _ => mem k l end end.
imports: Bool OrderedType SMT_classes ProofIrrelevance