fact: Fixpoint get_impl (k : var) (E : env A) {struct E} : option A := match E with | nil => None | (x,v) :: E' => If k = x then Some v else get_impl k E' end.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)