fact: Fixpoint find_expr_aux (e : expr) (n : nat) (l : list expr) := match l with | cons h t => if expr_beq e h then Some n else find_expr_aux e (S n) t | nil => None end.
imports: Coq(ZArith Reals List Psatz) Xreal Tree