proposition: Lemma fin_beq_dec {n} : forall (p : Fin.t n) (q : Fin.t n), fin_beq p q = true <-> p = q.
proof: Proof. intros; pattern n, p, q; eapply Fin.rect2; simpl; intuition; try (congruence || discriminate). - eapply Nat.eqb_refl. - eauto using Fin.FS_inj. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2