proposition: Lemma lf_injective f a b: lf_axiom f a b -> (forall u v, inc u a -> inc v a -> f u = f v -> u = v) -> injection (Lf f a b).
proof: Proof. move=> ta prop; split; first by apply: lf_function. by aw; move=> x y xs ys/=; do 2 rewrite LfV=>//; apply: prop. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)