proposition: Lemma Propagate_anonymous_ret__fast: forall {av A} (v : A) (tenv : Telescope av) tenv' env ext p, {{ tenv }} p {{ tenv' v }} ∪ {{ ext }} // env -> {{ tenv }} p {{ Cons NTNone (ret v) tenv' }} ∪ {{ ext }} // env.
proof: Proof. intros; rewrite Propagate_anonymous_ret; assumption. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas