fact: Example ex_reify_and_change (C : Category) (x y z w : C) (f : z ~> w) (g : y ~> z) (h : x ~> y) (i : x ~> z) : g ∘ h ≈ i -> f ∘ (id ∘ g ∘ h) ≈ (f ∘ g) ∘ h.
imports: Coq.Lists.List Category.Lib Category.Lib.IList Category.Theory.Category Category.Solver.Expr Category.Solver.Denote