proposition: Lemma last_default : forall (d1 : A) d2 l, l <> nil -> last l d1 = last l d2.
proof: Proof. induction l; simpl; intros. cong. destruct l. refl. apply IHl. discr. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)