proposition: Lemma wf_trans : forall (A : Set) (R : relation A) , well_founded R -> well_founded (trans_clos R).
proof: Proof. unfold well_founded; intros A R WR. intro; apply acc_trans; apply WR; trivial. Qed.
imports: Relations List