proposition: Lemma env_comp_empty_r : forall E, EmptyEnv [<->] E.
proof: Proof. intros; apply env_comp_sym; apply env_comp_empty. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)