proposition: Lemma nth_error_at_pos : forall (A : Type) l1 a l2, nth_error (l1 ++ a :: l2) (length l1) = @Some A a.
proof: Proof. intros A l1; induction l1 as [ | a1 l1]; intros a l2; simpl; trivial. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)