proposition: Lemma SameValues_add_SCA: forall av {A} (Wrp: FacadeWrapper (Value av) A) tel (st: StringMap.t (Value av)) k ext (v: A), (forall a, is_adt (wrap a) = false) -> k ∉ st -> st ≲ tel ∪ ext -> (StringMap.add k (wrap v) st) ≲ tel ∪ ext.
proof: Proof. induction tel; repeat (t_Morphism || SameValues_Facade_t). pose proof (H v); destruct (wrap v); try (simpl in *; congruence); SameValues_Facade_t. apply H; repeat (t_Morphism || SameValues_Facade_t). Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas