include "ground/relocation/gr_tl_eq_eq.ma".
include "ground/relocation/gr_isi.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Properties with gr_eq *********************************************************)
+(* Constructions with gr_eq *************************************************)
(*** isid_eq_repl_back *)
corec lemma gr_isi_eq_repl_back:
gr_eq_repl_fwd … gr_isi.
/3 width=3 by gr_isi_eq_repl_back, gr_eq_repl_sym/ qed-.
-(* Main inversion lemmas with gr_eq ****************************************************)
+(* Main inversions with gr_eq ***********************************************)
(*** isid_inv_eq_repl *)
corec theorem gr_isi_inv_eq_repl (g1) (g2): 𝐈❪g1❫ → 𝐈❪g2❫ → g1 ≡ g2.
/3 width=5 by gr_eq_push/
qed-.
-(* Alternative definition with gr_eq ***************************************************)
+(* Alternative definition with gr_eq ****************************************)
(*** eq_push_isid *)
corec lemma gr_eq_push_isi (f): ⫯f ≡ f → 𝐈❪f❫.