proposition: Lemma read_incl : forall A B (IB:Inhab B) (M N:map A B) i, i \indom M -> M \c N -> N[i] = M[i].
proof: Proof. Proof using. introv Hi HI. simpls. unfolds read_impl, incl_impl, dom_impl. rew_set in *. specializes HI i. destruct (N i) as [v|]. { destruct (M i) as [w|]; tryfalse. specializes HI w __. inverts* HI. } { destruct (M i) as [w|]; tryfalse. specializes HI w __. inverts* HI. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)