proposition: Lemma LList_dec: forall h :LList, Finite h -> forall k, Finite k -> {h=k}+{h<>k}.
proof: Proof. intros h H;elim H using Finite_rect. - intros k K ; elim K using Finite_rect. + left;auto. + right;discriminate. - intros x l H0 H1 k K ; elim K using Finite_rect. + right;discriminate. + intros x0 l0 H2 H3. destruct (H1 _ H2). * destruct (A_eq_dec x x0). subst x0 l; now left. right;intro H4;injection H4. intros;now destruct n. * right;intro H4;injection H4; intros;destruct n;auto. Qed.
imports: Eqdep Eqdep_dec EqdepFacts