proposition: Lemma inl_can_fun_prop S i j (f := isf S) (fi := inl_can_fun S i) (fj := inl_can_fun S j): gle (isr S) i j -> (fj \coP Vg f (J i j) /\ fi = fj \co (Vg f (J i j))).
proof: Proof. move => lij. move:(inl_prop4 lij) => [fij sij tij]. move:(inl_prop0 lij)=> [iE jE]. move:(inl_can_fun_fp iE) => [ffi si ti]. move:(inl_can_fun_fp jE) => [ffj sj tj]. have pd: source fj = target (Vg f (J i j)) by ue. have pe: fj \coP Vg f (J i j) by split. have pf:=(compf_f pe). have pg: target fi = target fj by rewrite ti tj. have ph: source fi = source (Vg f (J i j)) by ue. split => //; apply:function_exten => //; aw; trivial. move => x xsf /=; rewrite compfV//; last ue. rewrite ph sij in xsf. have vix: inc (Vf (Vg (isf S) (J i j)) x) (Vg (isE S) j) by Wtac. by rewrite /fi /fj !inl_can_fun_ev // (inl_class_of_fij lij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)