proposition: Lemma well_founded_R_comp : well_founded (transp R_Comp).
proof: Proof. set (w := Acc_ind (R := transp R) (fun M => forall T, proj1_sig T = M -> Acc (transp R_Comp) T )). intro T. apply w with (proj1_sig T); trivial. intros; constructor; intros. eapply H0 with (proj1_sig y); trivial. unfold R_Comp, transp in * . rewrite <- H1; trivial. apply comp_imp_acc. destruct T; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)