proposition: Lemma termineR2aux : termine R -> forall x, SN R2 x /\ (forall y, R y x -> SN R2 y).
proof: Proof. intros. apply Acc_ind with (R:=R) (P:=fun x => (SN R2 x) /\ (forall y, R y x -> (SN R2 y))). intuition. apply Acc_intro. intros. elim H2. intros. generalize (H1 z H3). intuition. generalize (H1 y H2). intuition. apply H. Qed.
imports: Coq(Lia Relations Wellfounded) CoLoR(term)