proposition: Lemma proj_bin_fun : forall A B C (f : CSetoid_bin_fun A B C) a, fun_strext (f a).
proof: Proof. intros A B C f a. red in |- *. elim f. intro fo. simpl. intros csbf_strext0 x y H. elim (csbf_strext0 _ _ _ _ H); intro H0. elim (ap_irreflexive _ _ H0). exact H0. Qed.
imports: CoRN.algebra.CSetoids