proposition: Lemma to_nat_eq_member_eq : forall {_ : EqDec T (@eq T)} x ls (a b : member x ls), to_nat a = to_nat b -> a = b.
proof: Proof. induction a; intros. { destruct (member_case b). { destruct H0. subst. rewrite (UIP_refl x0). reflexivity. } { destruct H0. subst. simpl in *. congruence. } } { destruct (member_case b). { exfalso. destruct H0. subst. simpl in *. congruence. } { destruct H0. subst. simpl in *. inversion H; clear H; subst. eapply IHa in H1. f_equal. assumption. } } Qed.
imports: Coq.Lists.List Relations RelationClasses ExtLib.Core.RelDec ExtLib.Data.SigT ExtLib.Data.ListNth ExtLib.Data.Option ExtLib.Tactics.Injection ExtLib.Tactics.EqDep