proposition: Lemma agree_below: forall A (e1 e2 : env A) x a k, lookup x e1 = Some a -> x < k -> agree e1 e2 k -> lookup x e2 = Some a.
proof: Proof. do 6 intro. intros hlookup ? ?. rewrite <- hlookup. symmetry. eauto. Qed.
imports: List Dblib(DblibTactics DeBruijn)