proposition: Lemma nth_error_singleton_in : forall (a b: A) i, nth_error (a :: nil) i = Some b -> a = b /\ i = 0.
proof: Proof. intros. destruct i. inversion H; auto. inversion H; destruct i; discr. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)