proposition: Lemma Propagate_anonymous_ret: forall {av A} (tenv' : A -> Telescope av) (ext : StringMap.t (Value av)) (vv : A), TelEq ext ([[ret vv as vv0]]::tenv' vv0) (tenv' vv).
proof: Proof. unfold TelEq; SameValues_Fiat_t. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas