proposition: Lemma TI_compose' k (G : graph k) : (G ⋅ TI_graph k) = G.
proof: Proof. extensionality f. apply TI_compose. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect