-| at_refl: â\88\80f,g,j1,j2. â\86\91f = g â\86\92 0 = j1 â\86\92 0 = j2 â\86\92 at g j1 j2
-| at_push: â\88\80f,i1,i2. at f i1 i2 â\86\92 â\88\80g,j1,j2. â\86\91f = g â\86\92 ⫯i1 = j1 â\86\92 ⫯i2 = j2 → at g j1 j2
-| at_next: â\88\80f,i1,i2. at f i1 i2 â\86\92 â\88\80g,j2. ⫯f = g â\86\92 ⫯i2 = j2 → at g i1 j2
+| at_refl: â\88\80f,g,j1,j2. ⫯f = g â\86\92 0 = j1 â\86\92 0 = j2 â\86\92 at g j1 j2
+| at_push: â\88\80f,i1,i2. at f i1 i2 â\86\92 â\88\80g,j1,j2. ⫯f = g â\86\92 â\86\91i1 = j1 â\86\92 â\86\91i2 = j2 → at g j1 j2
+| at_next: â\88\80f,i1,i2. at f i1 i2 â\86\92 â\88\80g,j2. â\86\91f = g â\86\92 â\86\91i2 = j2 → at g i1 j2