#n @(nat_ind_succ … n) -n /3 width=1 by gr_isf_tl/
qed.
(* Inversions with gr_tls ***************************************************)
(*** isfin_inv_tls *)
#n @(nat_ind_succ … n) -n /3 width=1 by gr_isf_tl/
qed.
(* Inversions with gr_tls ***************************************************)
(*** isfin_inv_tls *)