proposition: Lemma inf_A1: (forall l, inc l (domain c) -> has_inf_graph r (restr f (Vg c l))) -> (has_inf_graph r f <-> has_inf_graph r (Lg (domain c) (fun l => inf_graph r (restr f (Vg c l))))).
proof: Proof. move=> alsup. by split; move=> [x xs]; move: (inf_A x alsup) => aux; exists x; apply/aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)