proposition: Lemma env_subset_dropSuffix_length : forall E E', envSubset E' E -> length (dropEmptySuffix E') <= length E.
proof: Proof. intros. destruct (dropSuffix_last E') as [E'e | [A E'A]]. rewrite E'e; lia. set (E'd := dropSuffix_decl_rev E' E'A). set (w := H (pred (length (dropEmptySuffix E'))) A E'd). assert (Ed: nth_error E (pred (length (dropEmptySuffix E'))) <> None). inversion w; try_solve. set (x := proj1 (nth_in E (pred (length (dropEmptySuffix E')))) Ed). lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)