include "ground/relocation/gr_tls.ma".
include "ground/relocation/gr_pat_eq.ma".
-(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* POSITIVE APPLICATION FOR GENERIC RELOCATION MAPS *************************)
-(* Properties on tls ********************************************************)
+(* Constructions with gr_tls ************************************************)
(* Note: this requires ↑ on first n *)
(*** at_pxx_tls *)
]
qed-.
-(* Inversion lemmas with tls ************************************************)
+(* Inversions with gr_tls ***************************************************)
(* Note: this does not require ↑ on second and third p *)
(*** at_inv_nxx *)