(*** after_tls *)
lemma gr_after_tls_sn_tls (n):
∀f1,f2,f. @❪𝟏, f1❫ ≘ ↑n →
- f1 â\8a\9a f2 â\89\98 f â\86\92 ⫱*[n]f1 â\8a\9a f2 â\89\98 ⫱*[n]f.
+ f1 â\8a\9a f2 â\89\98 f â\86\92 â«°*[n]f1 â\8a\9a f2 â\89\98 â«°*[n]f.
#n @(nat_ind_succ … n) -n //
#n #IH #f1 #f2 #f #Hf1 #Hf
cases (gr_pat_inv_unit_succ … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1