proposition: Lemma SameValues_Fiat_Bind_TelEq_Pair : forall {av A1 A2 B} key compA compB tail ext, TelEq ext (Cons (av := av) key (@Bind (A1 * A2) B compA compB) tail) (Cons NTNone compA (fun a => Cons NTNone (ret (fst a)) (fun a1 => Cons NTNone (ret (snd a)) (fun a2 => Cons key (compB (a1, a2)) tail)))).
proof: Proof. unfold TelEq; repeat match goal with | _ => progress subst | _ => progress SameValues_Fiat_t_step | _ => rewrite <- surjective_pairing in * end. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas