proposition: Lemma isNotEmpty_dec : forall e, {isNotEmpty e} + {~isNotEmpty e}.
proof: Proof. intro e; destruct e. left; try_solve. right; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)