proposition: Corollary fin_beq_refl {m} : forall (p : Fin.t m), fin_beq p p = true.
proof: Proof. intros; eapply fin_beq_dec; reflexivity. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2