(*** isid_at_total *)
lemma gr_isi_pat_total: âf. đâȘfâ« â (âi1,i2. @âȘi1,fâ« â i2 â i1 = i2) â đâȘfâ«.
(*** isid_at_total *)
lemma gr_isi_pat_total: âf. đâȘfâ« â (âi1,i2. @âȘi1,fâ« â i2 â i1 = i2) â đâȘfâ«.