proposition: Lemma TelEq_let_ret2 {A1 A2 B av}: forall (xy: A1 * A2) (f: A1 -> A2 -> B) tenv (ext: StringMap.t (Value av)), TelEq ext ([[ ret (let (x, y) := xy in f x y) as fxy ]] :: tenv fxy) ([[ ret xy as xy ]] :: tenv (f (fst xy) (snd xy))).
proof: Proof. intros (? & ?) *. rewrite !Propagate_anonymous_ret; simpl. reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas