proposition: Lemma read_single : forall A B (IB:Inhab B) (k:A) (x:B), (k \:= x)[k] = x.
proof: Proof. Proof using. intros. unfold read, read_inst, read_impl. unfold single_bind, single_bind_inst, single_bind_impl. case_if*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)