proposition: Theorem termineR2 : termine R -> termine R2.
proof: Proof. intros rtermine. red. intros a. generalize (termineR2aux rtermine). intros hyp. decompose [and] (hyp a). auto. Qed.
imports: Coq(Lia Relations Wellfounded) CoLoR(term)