proposition: Lemma NotInTelescope_not_in_tail: forall {av A} s (val : Comp A) (tail : A -> Telescope av) (var : StringMap.key) (v : A), val ↝ v -> NotInTelescope var ([[ s ~~> val as kk]]::tail kk) -> NotInTelescope var (tail v).
proof: Proof. simpl; intros. intuition eauto. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.Core CertifiedExtraction.Utils Coq.Setoids.Setoid