proposition: Lemma injection_surjection_equipollent : forall {S T : Type} (f: S -> T) , injection f -> Csurjection f -> equipollent S T.
proof: Proof. Abort. Definition Fin (n:nat) := {m:nat & if lt_dec m n then unit else void}. Lemma Fin_eq: forall (n: nat) (fa fb : Fin n), (projT1 fa) = (projT1 fb) -> fa = fb. Proof. introv Heq. destruct fa as [a ap]. destruct fb as [b bp]. allsimpl. subst. apply eq_existsT with (ea := eq_refl). remember (lt_dec b n); destruct s; destruct ap, bp; auto. Qed.
imports: Coq.Init.Notations tactics Peano Basics Bool Arith Arith.EqNat Omega