fact: Fixpoint uf (r:env)(x:string)(n:Z){struct r} : option(env) := match r with nil => None | (y,n')::tl => if string_dec y x then Some((x,n)::tl) else bind (uf tl x n) (fun tl' => Some ((y,n')::tl')) end.
imports: ZArith List syntax Lia