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