proposition: Lemma Injex1_ff_p p: inc p r -> function_prop (Injex1_ff p) (Vg Injex1_E (P p)) (Vg Injex1_E (Q p)).
proof: Proof. move => pr; rewrite /Injex1_ff; saw. by apply: lf_function; apply: Injex1_ff_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)