proposition: Theorem fin_all_In : forall {n} (f : fin n), List.In f (fin_all n).
proof: Proof. induction n; intros. inversion f. remember (S n). destruct f. simpl; firstorder. inversion Heqn0. subst. simpl. right. apply List.in_map. auto. Qed.
imports: ExtLib.Core.RelDec ExtLib.Tactics.EqDep ExtLib.Tactics.Injection