proposition: Lemma inl_prop3 S y i j k (f:= isf S): gle (isr S) i j -> gle (isr S) j k -> inc y (Vg (isE S) i) -> Vf (Vg f (J j k)) (Vf (Vg f (J i j)) y) = Vf (Vg f (J i k)) y.
proof: Proof. move => lij ljk yv. have co:= (inl_prop2 lij ljk). move:(f_equal (Vf^~ y) (is_compose_f lij ljk)); rewrite compfV // => //. by move:(is_function_f lij) => [_ -> _];aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)