proposition: Lemma inl_can_fun_ev S i x: inc i (isI S) -> inc x (Vg (isE S) i) -> Vf (inl_can_fun S i) x = class (inl_equiv S) (J x i).
proof: Proof. by move => iI xE; rewrite /inl_can_fun LfV//; apply:inl_can_fun_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)