proposition: Lemma eq_cardinal_equiv: equivalence eq_cardinal.
proof: Proof. constructor. red; intro. destruct x. exists (fun x:T => x). red; split. red; intros. assumption. red; intro. exists y. reflexivity. red; intros. destruct H. inversion H0. destruct H1. destruct H3. exists (fun x:X => f0 (f x)). red; split. red; intros. apply H. apply H2. assumption. red; intro. destruct H. destruct H2. pose proof (H3 y). destruct H4. pose proof (H1 x). destruct H5. exists x0. rewrite H5. assumption. red; intros. destruct H. apply bijective_impl_invertible in H. destruct (function_inverse f H) as [finv]. destruct a. exists finv. apply invertible_impl_bijective. exists f. assumption. assumption. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec