proposition: Lemma becoming_empty {k} {l: list (graph k)} : becoming_transitive_closure [] l.
proof: Proof. unfold becoming_transitive_closure. intuition. inversion H. inversion H. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect