fact: Definition subst_dom (G: Subst) : Env := map (fun T => match T with | None => None | Some T => Some (type T) end) G.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)