proposition: Lemma LfV f a b c: lf_axiom f a b -> inc c a -> Vf (Lf f a b) c = f c.
proof: Proof. by move=> /lf_function ff ca; symmetry; apply:Vf_pr => //; apply: lf_graph2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)