proposition: Lemma WeakEq_add: forall (av : Type) (m1 m2 : StringMap.t (Value av)) (s0 : StringMap.key) (v : Value av), WeakEq m2 m1 -> WeakEq ([s0 |> v]::m2) ([s0 |> v]::m1).
proof: Proof. unfold WeakEq; t_Morphism; eauto using SameSCAs_add, SameADTs_add. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid