proposition: Lemma Propagate_ret : forall {av A} k (v: A) (tail: A -> Telescope av), TelStrongEq (Cons k (ret v) tail) (Cons k (ret v) (fun _ => tail v)).
proof: Proof. constructor. - reflexivity. - intros; computes_to_inv; subst; reflexivity. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.Core CertifiedExtraction.Utils Coq.Setoids.Setoid Eqdep