proposition: Lemma TI_compose k (G : graph k) : forall f, (G ⋅ TI_graph k) f = G f.
proof: Proof. induction k. unfold TI_graph. do 2 red in G. intros f; depelim f. intros f. depelim f. simp TI_graph graph_compose. destruct (G fz) as [[weight d]|]; simpl; try easy. now rewrite orb_false_r. simp TI_graph graph_compose. destruct (G (fs f)) as [[weight d]|]; simpl; trivial. now rewrite orb_false_r. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect