include "ground/relocation/gr_uni.ma".
include "ground/relocation/gr_isi_id.ma".
-(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* IDENTITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Properties with test for identity ****************************************)
+(* Constructions with gr_isi ************************************************)
(*** uni_inv_isid uni_isi *)
lemma gr_uni_isi (f): đźâšđ⩠⥠f â đâȘfâ«.
/2 width=1 by gr_eq_id_isi/ qed.
-(* Inversion lemmas with test for identity **********************************)
+(* Inversions with gr_isi ***************************************************)
(*** uni_isid isi_inv_uni *)
lemma gr_isi_inv_uni (f): đâȘfâ« â đźâšđ⩠⥠f.