proposition: Lemma Fin_decidable : forall (n:nat), Deq (Fin n).
proof: Proof. unfold Deq. intros. destruct (Nat.eq_dec (projT1 x) (projT1 y)) as [T|F];[left|right]. - apply Fin_eq; auto. - intro Heq. destruct F. destruct x. destruct y. inverts Heq. allsimpl. reflexivity. Defined.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega