proposition: Lemma last_nth : forall (d : A) l, last l d = nth (length l - 1) l d.
proof: Proof. induction l; simpl; intros. refl. rewrite IHl. elim l; simpl; intros. refl. destruct l0; simpl. refl. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)