proposition: Lemma inl_inductive_map_ev S u F i x: inl_map_compat S u F -> inc i (isI S) -> inc x (Vg (isE S) i) -> Vf (inductive_map S u F) (class (inl_equiv S) (J x i)) = Vf (Vg u i) x.
proof: Proof. move => ha. move:(inl_map_prop ha) => hb. move => iI xE; exact: (inl_map_property_res1 ha hb iI xE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)