Lemma IL-3. Inverse loop schema and basis imply β = α.

\{ \begin{matrix}x · ((((x · y′) · y)′ · z) · ((α · u)′ · (β · u))) = z \\ x′ · x = y′ · y \\ x′ · (x · y) = y \\ (x · y) · y′ = x \end{matrix} \} ⇒ \{β = α\}.

Proof (found by Otter 3.0.4 on gyro at 0.41 seconds).

1 β = α → □ 3 x · ((((x · y′) · y)′ · z) · ((α · u)′ · (β · u))) = z 5 x′ · x = y′ · y 6 x′ · (x · y) = y 8 (x · y) · y′ = x

11 x · ((((x · y′) · y)′ · z) · (u′ · (β · ((((α · v′) · v)′ · u)·

((α · w)′ · (β · w)))))) = z  [3 → 3]
19,18  (((x · y′) · y)′ · z) · ((α · u)′ · (β · u)) = x′ · z  [3 → 6, flip]
23  x · ((((x · y′) · y)′ · z) · (u′ · (β · (α′ · u)))) = z  [11 :19]
26  x · (x′ · y) = y  [3 :19]
31,30  x · (y · x)′ = y′  [6 → 8]
35,34  x′′ = x  [26 → 8 :31]
37,36  (x · y′) · y = x  [34 → 8]
40  x · ((x′ · y) · (z′ · (β · (α′ · z)))) = y  [23 :37]
48  x · (y′ · y) = x  [5 → 26]
52  (x′ · x) · y = y  [5 → 36 :35]
55,54  x · (y · y′) = x  [34 → 48]
61,60  (x · x′) · y = y  [34 → 52]
70  x · x′ = y · y′  [54 → 26]
84  x · (y′ · (β · (α′ · y))) = x  [70 → 40 :61,35]
126  x · (α′ · β) = x  [70 → 84 :35,55]
143  β = α  [26 → 126]
145  □  [143,1]