proposition: Lemma binds_get_or_arbitrary : forall `{Inhab A} x v (E:env A), binds x v E -> get_or_arbitrary x E = v.
proof: Proof. Proof using. introv M. unfold get_or_arbitrary. rewrite~ M. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)