proposition: Lemma tc_finite_sn x : Irreflexive (tc R) → pred_finite (tc R x) → sn R x.
proof: Proof. intros Hirr [xs Hfin]. remember (length xs) as n eqn:Hn. revert x xs Hn Hfin. induction (lt_wf n) as [n _ IH]; intros x xs -> Hfin. constructor; simpl; intros x' Hxx'. assert (x' ∈ xs) as (xs1&xs2&->)%elem_of_list_split by eauto using tc_once. refine (IH (length xs1 + length xs2) _ _ (xs1 ++ xs2) _ _); [rewrite app_length; simpl; lia..|]. intros x'' Hx'x''. opose proof* (Hfin x'') as Hx''; [by econstructor|]. cut (x' ≠ x''); [set_solver|]. intros ->. by apply (Hirr x''). Qed.
imports: stdpp(options)