proposition: Lemma dropLast_app : forall a (l1 l2: list A), dropLast (l1 ++ a :: l2) = l1 ++ dropLast (a :: l2).
proof: Proof. induction l1; trivial. intro. replace (dropLast ((a0 :: l1) ++ a :: l2)) with (a0 :: dropLast (l1 ++ a::l2)). rewrite (IHl1 l2); trivial. simpl. cut (l1 ++ a :: l2 <> nil). destruct (l1 ++ a :: l2); fo. auto with datatypes. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)