proposition: Lemma dropSuffix_decl_rev : forall E x A, dropEmptySuffix E |= x := A -> E |= x := A.
proof: Proof. intros. unfold dropEmptySuffix in H. destruct (option_dec (find_last isNotEmpty isNotEmpty_dec E)) as [Ee | [p Ep]]. rewrite Ee in H. destruct x; try_solve. rewrite Ep in H. unfold VarD; apply initialSeg_prefix with (S p); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)