(* Advanced constructions with pr_isi ***************************************)
(*** isid_at_total *)
-lemma pr_isi_pat_total: â\88\80f. ð\9d\90\93â\9dªfâ\9d« â\86\92 (â\88\80i1,i2. @â\9dªi1,fâ\9d« â\89\98 i2 â\86\92 i1 = i2) â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+lemma pr_isi_pat_total: â\88\80f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 (â\88\80i1,i2. @â\9d¨i1,fâ\9d© â\89\98 i2 â\86\92 i1 = i2) â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
#f #H1f #H2f @pr_isi_pat
#i lapply (H1f i) -H1f *
#j #Hf >(H2f … Hf) in ⊢ (???%); -H2f //