proposition: Lemma env_extend : forall M A, (copy (length M) None ++ A [#] EmptyEnv) [+] M = M ++ A [#] EmptyEnv.
proof: Proof. induction M; trivial. intro A. destruct a; simpl; rewrite IHM; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)