proposition: Lemma fun_strext (S': CSetoids.CSetoid) (f: T -> S'): Proper (equiv ==> @st_eq _) f -> @fun_strext CSetoid S' f.
proof: Proof. Proof with auto. red. simpl. repeat intro. apply <- (ax_ap_tight _ _ _ (cs_proof S') (f x) (f y))... Qed.
imports: CoRN.algebra.CSetoids Coq.Classes.SetoidDec Coq.Classes.Morphisms Coq.Classes.SetoidClass