include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_tls.ma".
-(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
-(* Properties with gr_eq ******************************************************)
+(* Constructions with gr_eq *************************************************)
(*** tls_eq_repl *)
lemma gr_tls_eq_repl (n):
- gr_eq_repl (λf1,f2. ⫱*[n] f1 â\89¡ ⫱*[n] f2).
+ gr_eq_repl (λf1,f2. â«°*[n] f1 â\89¡ â«°*[n] f2).
#n @(nat_ind_succ … n) -n /3 width=1 by gr_tl_eq_repl/
qed.