proposition: Corollary fin_beq_sym {n} : forall (p : Fin.t n) (q : Fin.t n), fin_beq p q = fin_beq q p.
proof: Proof. intros; case_eq (fin_beq p q); case_eq (fin_beq q p); intros; eauto. - apply fin_beq_neq_dec in H; apply fin_beq_dec in H0; congruence. - apply fin_beq_neq_dec in H0; apply fin_beq_dec in H; congruence. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2