proposition: Theorem wf_leftTrans : well_founded (leftTrans R).
proof: Proof. red. eapply Fix. eapply wf_R. clear. intros. constructor. intros. revert H. induction H0. { intros. eauto. } { intros. eapply IHleftTrans; clear IHleftTrans. intros. eapply H1. auto. eapply LTFin. auto. } Defined.
imports: ExtLib.Relations.TransitiveClosure