proposition: Lemma varDecl_single : forall x A B w, (copy x None ++ A[#]EmptyEnv) |= w := B -> A = B /\ x = w.
proof: Proof. intros. destruct (lt_eq_lt_dec x w) as [[xw | xw] | xw]. exfalso; apply (varD_UD_absurd H). left; apply nth_beyond; autorewrite with datatypes using simpl; try lia. rewrite xw; split; trivial. rewrite xw in H. unfold VarD in H. rewrite (@nth_app_right (option SimpleType) (copy w None) (A[#]EmptyEnv) w) in H; autorewrite with datatypes using auto. rewrite copy_length in H. replace (w - w) with 0 in H; [inversion H; trivial | lia]. exfalso; apply (varD_UD_absurd H). right; rewrite nth_app_left; autorewrite with datatypes using trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)