proposition: Lemma SameValues_Nil: forall {A} state ext, state ≲ (@Nil A) ∪ ext -> WeakEq ext state.
proof: Proof. simpl; intros; assumption. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid