proposition: Lemma list_app_first_last : forall l m (a : A), (l ++ a::nil) ++ m = l ++ a::m.
proof: Proof. induction l. auto. intros m a'. rewrite <- !app_comm_cons. destruct (IHl m a'); trivial. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)