-lemma at_inv_nxn: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
- (∃∃g. @⦃j1, g⦄ ≘ j2 & ⫯g = f) ∨
- ∃∃g. @⦃i1, g⦄ ≘ j2 & ↑g = f.
+lemma at_inv_nxn: ∀f,i1,i2. @⦃i1,f⦄ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
+ (∃∃g. @⦃j1,g⦄ ≘ j2 & ⫯g = f) ∨
+ ∃∃g. @⦃i1,g⦄ ≘ j2 & ↑g = f.