fact: Fixpoint NotInTelescope {av} k (tenv: Telescope av) := match tenv with | Nil => True | Cons _ key val tail => Some k <> (NameTagAsStringOption key) /\ (forall v, val ↝ v -> NotInTelescope k (tail v)) end.
imports: Coq.Classes.Morphisms CertifiedExtraction.Core CertifiedExtraction.Utils Coq.Setoids.Setoid