proposition: Lemma etp_axiom f: correspondence f -> lf_axiom (Vfs f) (\Po (source f)) (\Po (target f)).
proof: Proof. move=> cf x /setP_P xs; apply/setP_P. apply: (@sub_trans (range (graph f))); fprops; apply: dirim_Sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)