proposition: Lemma sub_inl (a b : T1) (p : @Path (sjoin T1 T2) (inl a) (inl b)) : {subset p <= codom inl}.
proof: Proof. apply: path_closed; first by rewrite codom_f. do 2 case => ? //; rewrite ?codom_f //. by case/codomP => ?. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)