proposition: Lemma TelEq_same_wrap : forall {av A1 A2} {W1: FacadeWrapper (Value av) A1} {W2: FacadeWrapper (Value av) A2} (x1: A1) (x2: A2), wrap x1 = wrap x2 -> forall (t: Telescope av) ext k, TelEq ext (Cons (NTSome k) (ret x1) (fun _ => t)) (Cons (NTSome k) (ret x2) (fun _ => t)).
proof: Proof. split; SameValues_Fiat_t. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas