proposition: Lemma Re_co_do_strext : forall (X Z : CSetoid) (f : CSetoid_fun X Z), fun_strext (Re_co_do X Z f).
proof: Proof. intros X Z f. unfold fun_strext in |- *. intros x y. simpl in |- *. apply (csf_strext X Z f). Qed.
imports: CoRN.metrics.Prod_Sub