proposition: Lemma eq_app_elim_r : forall l1 l l2, l = l1 ++ l2 -> l2 = sub_list l (length l1) (length l2).
proof: Proof. induction l1; simpl; intros. subst l2. induction l; simpl; intros. refl. rewrite <- IHl. refl. destruct l. discr. inversion H. subst. simpl. apply IHl1. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)