proposition: Lemma emptyEnv_copyNone : forall k, emptyEnv (copy k None).
proof: Proof. intros; intro p. destruct (le_gt_dec k p). left; apply nth_beyond; autorewrite with datatypes using trivial. right; apply nth_copy_in; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)