include "ground/relocation/gr_tl_eq.ma".
include "ground/relocation/gr_uni.ma".
-(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* UNIFORM ELEMENTS FOR GENERIC RELOCATION MAPS *****************************)
-(* Inversion lemmas with gr_eq ***************************************************)
+(* Inversions with gr_eq ****************************************************)
(*** uni_inv_push_dx *)
lemma gr_eq_inv_uni_push (n) (g): š®āØnā© ā” ā«Æg ā ā§ā§ š = n & š¢ ā” g.
lemma gr_eq_inv_next_uni (n) (g): āg ā” š®āØnā© ā ā§ā§ š®āØānā© ā” g & āān = n.
/3 width=1 by gr_eq_inv_uni_next, gr_eq_sym/ qed-.
-(* Inversion lemmas with id and gr_eq *)
+(* Inversions with gr_id and gr_eq ******************************************)
(*** uni_inv_id_dx *)
lemma gr_eq_inv_uni_id (n): š®āØnā© ā” š¢ ā š = n.