proposition: Lemma env_eq_empty_tail : forall E n, E [=] E ++ copy n None.
proof: Proof. intros; split; intros p A D. unfold VarD; rewrite nth_app_left; trivial. apply nth_some with (Some A); trivial. destruct (nth_app E (copy n None) p D) as [[Dl _] | [Dr _]]. trivial. destruct (le_gt_dec n (p - length E)). assert (p - length E >= length (copy n (None (A:=SimpleType)))). autorewrite with datatypes using lia. set (w := nth_beyond (copy n None) H). try_solve. set (w := nth_copy_in (None (A:=SimpleType)) g). try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)