proposition: Theorem fin_case : forall n (f : fin (S n)), f = F0 \/ exists f', f = FS f'.
proof: Proof. intros. generalize (fin_all_In f). intros. destruct H; auto. eapply List.in_map_iff in H. right. destruct H. exists x. intuition. Qed.
imports: ExtLib.Core.RelDec ExtLib.Tactics.EqDep ExtLib.Tactics.Injection