proposition: Lemma SameValues_Nil_always: forall {A} state, state ≲ (@Nil A) ∪ state.
proof: Proof. simpl; firstorder. Qed.
imports: CertifiedExtraction.HintDBs CertifiedExtraction.Core CertifiedExtraction.Utils CertifiedExtraction.StringMapUtils Coq.Setoids.Setoid