proposition: Lemma graphs_relation_compose {k} (g g' : list (graph k)) x y z : graphs_relation g x z -> graphs_relation g' z y -> graphs_relation (compose_family g g') x y.
proof: Proof. intros gxz gzy. induction g in g', x, y, z, gxz, gzy |- *; simp compose_family. unfold graphs_relation in gxz. simpl in gxz. destruct gxz. unfold graphs_relation. unfold compose_family. rewrite -> map_app, map_map, list_union_app. left. apply (union_graph_relation_compose _ _ _ _ z H gzy). specialize (IHg g' x y z H gzy). unfold graphs_relation. rewrite -> map_app, map_map, list_union_app. right; auto. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect