proposition: Lemma env_comp_single : forall A x E, (E |= x :! \/ E |= x := A) -> (copy x None ++ A [#] EmptyEnv) [<->] E.
proof: Proof. intros; intros p B C Dl Dr. destruct (lt_eq_lt_dec p x) as [[p_x | p_x] | p_x]. exfalso; apply (varD_UD_absurd Dl). right; unfold VarUD. rewrite nth_app_left. apply nth_copy_in; trivial. autorewrite with datatypes using trivial. inversion H. exfalso; apply (varD_UD_absurd Dr). rewrite p_x; trivial. rewrite <- p_x in H0. inversion Dl. assert (A = B). cut ((copy x None ++ A[#]EmptyEnv) |= p := B); trivial. unfold VarD. rewrite nth_app_right; autorewrite with datatypes using try lia. rewrite p_x; rewrite Nat.sub_diag. intro D; inversion D; trivial. inversion Dr; inversion H0; try_solve. exfalso; apply (varD_UD_absurd Dl). left; unfold VarUD. rewrite nth_app_right; autorewrite with datatypes. cut (p - x > 0); try lia. destruct (p - x); intro; try solve [lia]. destruct n; trivial. lia. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)