proposition: Lemma union_graph_relation_compose {k} x y a (g : list (graph k)) z: graph_relation a x z -> list_union (map graph_relation g) z y -> list_union (map (fun x => graph_relation (a ⋅ x)) g) x y.
proof: Proof. induction g; simpl. 1:firstorder. intros Hxz Hzy. destruct Hzy. specialize (graph_relation_compose x y a a0). left; firstorder. firstorder. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect