fact: Fixpoint fin_all (n : nat) : list (fin n) := match n as n return list (fin n) with | 0 => nil | S n => @F0 n :: List.map (@FS _) (fin_all n) end%list.
imports: ExtLib.Core.RelDec ExtLib.Tactics.EqDep ExtLib.Tactics.Injection