proposition: Lemma Nth_app_inv : forall n x l1 l2, Nth n (l1++l2) x -> (Nth n l1 x) \/ (exists m, n = length l1 + m /\ Nth m l2 x).
proof: Proof. Proof using. introv. gen n. induction l1; introv H; rew_list in H. { right. rew_list. exists~ n. } { inverts H. { left~. } { forwards* M: IHl1. destruct M as [|(m&?&?)]. { left~. } { right*. rew_list. exists m. split~. math. } } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)