proposition: Theorem fpfa_fb: bijection (first_partial_map).
proof: Proof. set f:= first_partial_map. have sf:source f = fBCA by rewrite /f /first_partial_map; aw. have tf: target f = functions C fBA by rewrite /f /first_partial_map; aw. have ff:= fpfb_f. split;split=>//. move=> x y; rewrite sf=> xs ys eq. have sx: source x = B \times C by move /functionsP: xs => [_ ]. have sy: source y = B \times C by move /functionsP: ys => [_ ]. have ha: forall z, inc z (source x) -> Vf x z = Vf y z. rewrite sx => z zp. by rewrite -(fpfb_VV xs zp) -(fpfb_VV ys zp) eq. move: xs ys => /functionsP [fx _ tx] /functionsP [fy _ ty]. by apply: function_exten=>//; try ue. move=> y yt. set (g:= Lf (fun x => Vf (Vf y (Q x)) (P x)) (B \times C) A). have ta: lf_axiom (fun x => Vf (Vf y (Q x) ) (P x)) (B \times C) A. move=> x /setX_P [xp pa qb]. move: yt; rewrite tf; move /functionsP => [fy sy ty]. have: (inc (Vf y (Q x)) (target y)) by Wtac. by rewrite ty; move /functionsP=> [fW sW <-]; Wtac. have gsf: (inc g (source f)). by rewrite /g sf; apply /functionsP; hnf;aw; split => //; apply: lf_function. ex_tac. have: inc (Vf f g) (target f) by Wtac. move:yt; rewrite tf;move=> /functionsP [fy sy ty] /functionsP [fW sW tw]. apply: function_exten => //;try ue; move => x; rewrite sy=> xs. have: inc (Vf (Vf f g) x) (target (Vf f g)) by Wtac. have: inc (Vf y x) (target y) by Wtac. rewrite tw ty; move=> /functionsP [fy1 sy1 ty1] /functionsP [fW1 sW1 tw1]. apply: function_exten=>//; try ue; rewrite sy1=> z zs. have psg: (inc (J z x) (source g)) by rewrite /g; aw; fprops. rewrite/g lf_source in psg; rewrite sf in gsf. move: (fpfb_VV gsf psg); aw; move=> ->. by rewrite /g LfV; first by aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)