fact: Definition dropEmptySuffix (E: Env) : Env := match find_last isNotEmpty isNotEmpty_dec E with | None => EmptyEnv | Some i => initialSeg E (S i) end.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)