proposition: Lemma tc_unique X: uniqueness (transitive_closure_pr X).
proof: Proof. move => a b [p1 p2 p3] [q1 q2 q3]. apply: extensionality; [by apply:p3 | by apply:q3]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)