proposition: Corollary fin_beq_trans {n} : forall (p q r : Fin.t n), fin_beq p q = true -> fin_beq q r = true -> fin_beq p q = true.
proof: Proof. repeat setoid_rewrite fin_beq_dec; congruence. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2