proposition: Lemma ex_loop_tc x : ex_loop (tc R) x ↔ ex_loop R x.
proof: Proof. split. - revert x; cofix IH. intros x (y & Hstep & Hloop')%ex_loop_inv. destruct Hstep as [x y Hstep|x y z Hstep Hsteps]. + econstructor; eauto. + econstructor; [by eauto|]. eapply IH. econstructor; eauto. - revert x; cofix IH. intros x (y & Hstep & Hloop')%ex_loop_inv. econstructor; eauto using tc_once. Qed.
imports: stdpp(options)