proposition: Lemma agree_concat: forall A (e : list A) (e1 e2 : env A) k n, agree e1 e2 k -> k + length e = n -> agree (concat e1 e) (concat e2 e) n.
proof: Proof. induction e; simpl; intros. replace n with k by omega. assumption. eauto using agree_insert with omega. Qed.
imports: List Dblib(DblibTactics DeBruijn)