proposition: Lemma dropSuffix_last : forall E (E' := dropEmptySuffix E), length E' = 0 \/ exists A, E' |= pred (length E') := A.
proof: Proof. intro E. unfold dropEmptySuffix. destruct (option_dec (find_last isNotEmpty isNotEmpty_dec E)) as [Ee | [p Ep]]. rewrite Ee; left; trivial. rewrite Ep; right. destruct (find_last_ok isNotEmpty isNotEmpty_dec E Ep) as [w [pEpw wSome]]. destruct w. exists s. autorewrite with datatypes. rewrite Nat.min_l. unfold VarD. rewrite initialSeg_nth; trivial. auto with arith. assert (nth_error E p <> None); try_solve. set (w := proj1 (nth_in E p) H). lia. destruct wSome; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)