proposition: Lemma Lifted_MapsTo_neq: forall `{FacadeWrapper (Value av) A} `{FacadeWrapper (Value av) A'} ext k (v: A) tail k' (v': A'), k <> k' -> @Lifted_MapsTo av ext (tail v) k' (wrap v') -> @Lifted_MapsTo av ext (Cons (NTSome k) (ret v) tail) k' (wrap v').
proof: Proof. unfold Lifted_MapsTo, LiftPropertyToTelescope; intros. SameValues_Facade_t. eauto using StringMap.remove_3. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.FacadeNotations CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.ExtendedLemmas