proposition: Lemma two_projections_ax a b c: lf_axiom (fun z => (J (first_projection z a b) (secnd_projection z a c))) (functions a (b \times c)) ((functions a b) \times (functions a c)).
proof: Proof. move=> t /functionsP [ft st tt]. move: (two_projections_aux ft st tt)=> [_ _ fa fb _]. by apply: setXp_i; apply /functionsP;split => //; rewrite /first_projection /secnd_projection; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)