proposition: Lemma bin_fun_strext (S'': CSetoids.CSetoid) (f: T -> T' -> S''): Proper (equiv ==> equiv ==> @st_eq _) f -> bin_fun_strext CSetoid CSetoid S'' f.
proof: Proof. Proof with auto. red. simpl. intros. destruct (eq_dec x1 x2)... destruct (eq_dec' y1 y2)... exfalso. apply <- (ax_ap_tight _ _ _ (cs_proof S'') (f x1 y1) (f x2 y2))... rewrite -> e, e0. reflexivity. Qed.
imports: CoRN.algebra.CSetoids Coq.Classes.SetoidDec Coq.Classes.Morphisms Coq.Classes.SetoidClass