#f21 #f1 #f #g21 [1,2: #g1 ] #g #Hf #H21 [1,2: #H1 ] #H #g22 #H0
[ cases (eq_inv_px … H0 … H21) -g21 /3 width=7 by after_refl/
| cases (eq_inv_px … H0 … H21) -g21 /3 width=7 by after_push/
-| cases (eq_inv_nx … H0 … H21) -g21 /3 width=5 by after_next/
+| cases (eq_inv_nx … H0 … H21) -g21 /3 width=5 by after_next/
]
qed-.
(* Properties on tls ********************************************************)
-lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≘ n →
+lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≘ n →
f1 ⊚ f2 ≘ f → ⫱*[n]f1 ⊚ f2 ≘ ⫱*[n]f.
#n elim n -n //
#n #IH #f1 #f2 #f #Hf1 #Hf