include "ground/relocation/gr_isi_pat.ma".
include "ground/relocation/gr_ist.ma".
-(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* TOTALITY CONDITION FOR GENERIC RELOCATION MAPS ***************************)
-(* Advanced properties on isid **********************************************)
+(* Advanced constructions with gr_isi ***************************************)
(*** isid_at_total *)
lemma gr_isi_pat_total: âf. đâȘfâ« â (âi1,i2. @âȘi1,fâ« â i2 â i1 = i2) â đâȘfâ«.