proposition: Lemma SameValues_Dealloc_SCA : forall {av} {A} (Wrp: FacadeWrapper (Value av) A) st k (v: Comp A) tail ext, (forall a, is_adt (wrap a) = false) -> st ≲ Cons (av := av) (NTSome k) v tail ∪ ext -> st ≲ Cons NTNone v tail ∪ ext.
proof: Proof. SameValues_Fiat_t. StringMap_t. repeat match goal with | [ H: StringMap.MapsTo _ _ ?st |- ?st ≲ _ ∪ _ ] => rewrite (MapsTo_add_remove H) | [ H: is_adt ?v = false |- _ ] => destruct v; simpl in H; try congruence | [ H: match ?x with _ => _ end = _ |- _ ] => destruct x; try congruence end. apply SameValues_add_SCA; eauto using StringMap.remove_1. Qed.
imports: Coq.Classes.Morphisms CertifiedExtraction.CoreLemmas CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.PropertiesOfTelescopes CertifiedExtraction.FacadeLemmas