fact: Fixpoint update {K V} {kRealDec:RelDec (@eq K)} x v l : list (K * V) := match l with | [] => [(x,v)] | (y,w)::l' => if eq_dec x y then (x,v)::l' else (y,w)::update x v l' end.
imports: List String ExtLib.Structures.Monads ExtLib.Core.RelDec