proposition: Lemma Finite_Finite_alt : forall x, Finite x -> Finite_alt x.
proof: Proof. intros x H;induction H. - constructor; intros a y H;inversion H. - constructor;intros b y;injection 1; intros;subst y;assumption. Qed.
imports: List Extraction