proposition: Lemma Injex1_ff_ax p : inc p r -> lf_axiom (fun f => restriction f (Vg V (Q p))) (Vg Injex1_E (P p)) (Vg Injex1_E (Q p)).
proof: Proof. move => pr f. move: (pr1_sr pr)(pr2_sr pr); rewrite sr => pI qI. move:(proj31 or _ pr) => pp; move:(pr); rewrite -{1}pp => gle1. rewrite /Injex1_E ! LgV//; move/functionsP => [ff sf tf]. move:(proj44 Vprop _ _ gle1); rewrite -{1} sf => sub1. apply/functionsP; rewrite - tf;exact:(restriction_prop ff sub1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)