proposition: Lemma dropSuffix_decl : forall E x A, E |= x := A -> dropEmptySuffix E |= x := A.
proof: Proof. intros. destruct (find_last_last isNotEmpty isNotEmpty_dec E x H) as [q [Eq qx]]; try_solve. unfold dropEmptySuffix. rewrite Eq. unfold VarD; rewrite initialSeg_nth; trivial. lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)