proposition: Lemma bool2_Equi : equipollent bool (Fin 2).
proof: Proof. Abort. Definition Finite (T : Type) := {n:nat $ equipollent ( Fin n) T}. Lemma Finite_Deq : forall (A:Type), Finite A -> Deq A. Proof. introv Hf. repnud Hf. exrepnd. eapply equipollent_Deq. apply Fin_decidable. exact Hf0. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega