fact: Fixpoint DropName {A} k (t: Telescope A) := match t with | Nil => Nil | Cons T key val tail => Cons (match key with | NTSome _key H => if string_dec _key k then NTNone else key | NTNone => key end) val (fun v => (DropName k (tail v))) end.
imports: Coq.Classes.Morphisms CertifiedExtraction.Core CertifiedExtraction.Utils Coq.Setoids.Setoid