proposition: Lemma comp_resp_bij : forall A B C f g, bijective f -> bijective g -> bijective (compose_CSetoid_fun A B C f g).
proof: Proof. intros A B C f g. intros H0 H1. elim H0; clear H0; intros H00 H01. elim H1; clear H1; intros H10 H11. split. intros a0 a1; simpl; intro. apply H10; apply H00; auto. intro c; simpl. elim (H11 c); intros b H20. elim (H01 b); intros a H30. exists a. Step_final (g b). Qed.
imports: CoRN.algebra.CSetoids