proposition: Lemma agrees_on_covering f x g g': covering f x -> function g -> function g' -> source g = x -> source g' = x -> (forall i, inc i (domain f) -> agrees_on (x \cap (Vg f i)) g g') -> agrees_on x g g'.
proof: Proof. move=> [fgf c] fg fg' sg sg' ag. hnf; rewrite sg sg';split; fprops. move=> a ax; move /setUb_P: (c _ ax) => [y ysf afy]. by apply: (proj33 (ag _ ysf)); apply: setI2_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)