include "ground/relocation/gr_nexts.ma".
include "ground/relocation/gr_isd.ma".
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with iterated next ********************************************)
+(* Constructions with gr_nexts **********************************************)
(*** isdiv_nexts *)
lemma gr_isd_nexts (n) (f): šāŖfā« ā šāŖā*[n]fā«.
#n @(nat_ind_succ ā¦ n) -n /3 width=3 by gr_isd_next/
qed.
-(* Inversion lemmas with iterated next **************************************)
+(* Inversions with gr_nexts *************************************************)
(*** isdiv_inv_nexts *)
lemma gr_isd_inv_nexts (n) (g): šāŖā*[n]gā« ā šāŖgā«.