proposition: Lemma finite_inj : forall i j, F i = F j -> i = j.
proof: Proof. intros i j H; case (lt_eq_lt_dec i j). - destruct 1. + case (@lt_irrefl (F i)). * pattern (F i) at 2 ; rewrite H. apply finite_mono;auto. + auto. - intro; case (@lt_irrefl (F i)). pattern (F i) at 1 ; rewrite H; apply finite_mono;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)