fact: Fixpoint find {A: Type} {EA: EquivDec.EqDec A eq} (l : list A) (n : A) (ans : Z) := match l with | [] => ans | h :: t => if EA h n then ans else (find t n (1 + ans)) end.
imports: VST.floyd.proofauto Coq.Classes.Equivalence CertiGraph.lib.List_ext