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