proposition: Lemma Nth_functional : forall n l x1 x2, Nth n l x1 -> Nth n l x2 -> x1 = x2.
proof: Proof. Proof using. introv H1. induction H1; intro H2; inverts~ H2. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)