proposition: Lemma noCycle_T x y : x = y -> noSubterm_T x y with noCycle_R x y : x = y -> noSubterm_R x y.
proof: Proof. * intros ->. destruct y. - exact I. - refine (I, _). change (noSubterm_TR (N x) x). apply step_N. apply noCycle_R. reflexivity. * intros ->. destruct y. - exact I. - split. + refine (I, _). change (noSubterm_RT (rcons t y) t). apply step_rcons1. apply noCycle_T. reflexivity. + apply step_rcons2. apply noCycle_R. reflexivity. Qed.
imports: Equations(Equations) Below