fact: Fixpoint ALKeepFirst (sub : AssocList) (vars : list Key) : AssocList := match sub with | nil => nil | (v, t) :: xs => if in_deq _ DeqKey v vars then (v, t) :: ALKeepFirst xs (diff DeqKey [v] vars) else ALKeepFirst xs vars end.
imports: list Omega