include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_sle.ma".
-(* INCLUSION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* INCLUSION FOR GENERIC RELOCATION MAPS ************************************)
-(* Properties with iterated tail ********************************************)
+(* Constructions with gr_tls ************************************************)
(*** sle_tls *)
lemma gr_sle_tls:
- â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 â\88\80n. ⫱*[n] f1 â\8a\86 ⫱*[n] f2.
+ â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 â\88\80n. â«°*[n] f1 â\8a\86 â«°*[n] f2.
#f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n
/2 width=5 by gr_sle_tl/
qed.