proposition: Lemma Nth_cons_inv : forall n x y q, Nth n (y::q) x -> (n = 0 /\ x = y ) \/ (exists m, n = m+1 /\ Nth m q x).
proof: Proof. Proof using. introv H. inverts H. { left*. } { right. exists n0. splits~. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)