#n2 @(nat_ind_succ … n2) -n2
[ /4 width=4 by gr_pat_eq_repl_back, gr_pat_refl, ex_intro/
| #n2 #IH #f <gr_tls_swap <gr_tls_swap in ⊢ (??%→?); #H
#n2 @(nat_ind_succ … n2) -n2
[ /4 width=4 by gr_pat_eq_repl_back, gr_pat_refl, ex_intro/
| #n2 #IH #f <gr_tls_swap <gr_tls_swap in ⊢ (??%→?); #H