fact: Fixpoint fin_eq_dec {n} (x : fin n) {struct x} : fin n -> bool := match x in fin n' return fin n' -> bool with | F0 _ => fun y => match y with | F0 _ => true | _ => false end | FS n' x' => fun y : fin (S n') => match y in fin n'' return (match n'' with | 0 => unit | S n'' => fin n'' end -> bool) -> bool with | F0 _ => fun _ => false | FS _ y' => fun f => f y' end (fun y => fin_eq_dec x' y) end.
imports: ExtLib.Core.RelDec ExtLib.Tactics.EqDep ExtLib.Tactics.Injection