proposition: Lemma tc_exists X: transitive_closure_pr X (transitive_closure X).
proof: Proof. rewrite /transitive_closure. move: (induction_defined_pr union X) => []. set f := induction_defined _ _; set Y := union (target f) => sf [ff sjf] f0 fs. have yp: forall y, inc y Y <-> exists2 n, inc n Nat & inc y (Vf f n). rewrite - sf;move => y; split. move /setU_P => [z zy /sjf [x xsf fx]]; ex_tac; ue. move => [n nsf yv]; apply /setU_P; exists (Vf f n) => //; Wtac. split. move => t /yp [n nN tv] s st; apply/yp; exists (csucc n). by apply:NS_succ. rewrite (fs _ nN); union_tac. rewrite -f0;move => t tX; apply /yp; exists \0c => //; apply:NS0. move => Z tz xz. have aux: forall n, inc n Nat -> sub (Vf f n) Z. apply: Nat_induction; first by ue. by move => n nN h; rewrite (fs _ nN); apply: setU_s2 => y /h /tz. move => t /yp [n /aux]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)