fact: Definition cons_unique (e : expr) (l : list expr) := let fix aux (l' : list expr) := match l' with | cons h t => if expr_beq e h then l else aux t | nil => cons e l end in aux l.
imports: Coq(ZArith Reals List Psatz) Xreal Tree