proposition: Lemma NotInTelescope_not_eq_head: forall `{FacadeWrapper (Value av) A} (key : string) (val : Comp A) (tail : A -> Telescope av) (var : StringMap.key), NotInTelescope var ([[` key ~~> val as kk]]::tail kk) -> key <> var.
proof: Proof. simpl; intros; repeat cleanup; eauto. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.Core CertifiedExtraction.Utils Coq.Setoids.Setoid