proposition: Lemma CK4F_induced2 (G : graph2) (V : {set G}) : @connected G V -> CK4F G -> CK4F (induced2 V).
proof: Proof. move=> V_conn G_CK4F. rewrite /induced2. case: {-}_ / idP => // i_V. case: {-}_ / idP => // o_V. split; first exact: connected_induced. case: G_CK4F => _. apply: subgraph_K4_free. exists val; first exact: val_inj. move=> x y xy _. move: xy. rewrite /edge_rel/= -!(inj_eq val_inj) /=. case/or3P=> [xy|->|->] //. apply/orP. left. pattern x, y. revert x y xy. apply skelP; first by move=> x y xy; rewrite sgP. move=> e. rewrite /edge_rel/=/sk_rel -!(inj_eq val_inj)/= => -> /=. exact: adjacent_edge. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)