proposition: Lemma wf_tclosure : forall A (R:binary A), wf R -> wf (tclosure R).
proof: Proof. Proof using. unfold wf, well_founded. introv HAcc. intro a. specializes HAcc a. generalize dependent a. induction 1 as [ a _ IH ]. constructor. intros b Hba. generalize a b Hba IH. clear a b Hba IH. induction 1; eauto using Acc_inv. Qed.
imports: TLC(LibTactics LibLogic LibProd LibSum LibRelation LibNat LibInt)