proposition: Lemma nth_error_weaken : forall ls' (ls : list T) n v, nth_error ls n = Some v -> nth_error (ls ++ ls') n = Some v.
proof: Proof. clear. induction ls; destruct n; simpl; intros; unfold value, error in *; try congruence; auto. Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat