From stdpp Require Import strings. From iris.base_logic Require Import lib.iprop. Require uses context expr. Module context := context.context_simpl_impl uses.uses. Module Export expr := (expr.expr context). Export uses.uses.