include "ground/relocation/gr_tl_eq_eq.ma".
include "ground/relocation/gr_isd.ma".
-(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* DIVERGENCE CONDITION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
(*** isdiv_eq_repl_back *)
corec lemma gr_isd_eq_repl_back:
gr_eq_repl_fwd … gr_isd.
/3 width=3 by gr_isd_eq_repl_back, gr_eq_repl_sym/ qed-.
-(* Main inversion lemmas with gr_eq ***************)
+(* Main inversions with gr_eq ***********************************************)
(*** isdiv_inv_eq_repl *)
corec theorem gr_isd_inv_eq_repl (g1) (g2): 𝛀❪g1❫ → 𝛀❪g2❫ → g1 ≡ g2.
/3 width=5 by gr_eq_next/
qed-.
-(* Alternative definition with gr_eq ***************************************************)
+(* Alternative definition with gr_eq ****************************************)
(*** eq_next_isdiv *)
corec lemma gr_eq_next_isd (f): ↑f ≡ f → 𝛀❪f❫.