proposition: Lemma nth_in2: forall (A : Type) (n : nat) (l : list A) (a d : A), n < length l -> (nth n l d) = a -> LIn a l.
proof: Proof. introns XX. pose proof (nth_in _ n l d XX) as XY. congruence. Qed.
imports: UsefulTypes bin_rels Omega