proposition: Corollary fin_beq_neq_dec {n} : forall (p : Fin.t n) (q : Fin.t n), fin_beq p q = false <-> p <> q.
proof: Proof. intros; setoid_rewrite <- fin_beq_dec; split; intros; destruct (fin_beq p q); congruence. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2