proposition: Theorem tree_helly (F : {set {set G}}) : (forall T : {set G}, T \in F -> connected T) -> F != set0 -> {in F &, forall A B, A :&: B != set0} -> \bigcap_(A in F) A != set0.
proof: Proof. rewrite -card_gt0. move => F_subtree F_inh F_pq_in. case: (@helly3_lifting G (@connected G) _ _ F _ _ _) => //. - exact: tree_connectI. - exact: tree_I3. - move => x Hx. apply/set0Pn. exists x. apply/bigcapP. exact: Hx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph set_tac)