bs ; a.as' a.(as' @ bs) (recursive)
Thm* 
R:(Alph*
Alph*Prop), n:
, L:(Alph*
), m:.
(x:Alph*. R(x,x))
& (x,y:Alph*. R(x,y) 
R(y,x))
& (x,y,z:Alph*. R(x,y) & R(y,z) R(x,z))
& (x,y,z:Alph*. R(x,y) R((z @ x),z @ y))
& (
w:(nAlph*). l:Alph*. i:n. R(l,w(i)))
& (v:(mAlph*). l:Alph*. L(l) 
(i:m. R(l,v(i))))
& Fin(Alph)
(x,y:Alph*. Dec(l:Alph*. L(l @ x) = L(l @ y)))
auto2_lemma_8
Thm* R:(Alph*Alph*Prop), n:, L:(Alph*), m:.
(x:Alph*. R(x,x))
& (x,y:Alph*. R(x,y) R(y,x))
& (x,y,z:Alph*. R(x,y) & R(y,z) R(x,z))
& (x,y,z:Alph*. R(x,y) R((z @ x),z @ y))
& (w:(nAlph*). l:Alph*. i:n. R(l,w(i)))
& (v:(mAlph*). l:Alph*. L(l) (i:m. R(l,v(i))))
& Fin(Alph)
(x,y:Alph*. Dec(l:Alph*. 
L(l @ x) = L(l @ y)))
auto2_lemma_7
Thm* R:(Alph*Alph*Prop), n:.
(x:Alph*. R(x,x))
& (x,y:Alph*. R(x,y) R(y,x))
& (x,y,z:Alph*. R(x,y) & R(y,z) R(x,z))
& (x,y,z:Alph*. R(x,y) R((z @ x),z @ y))
& (w:(nAlph*). l:Alph*. i:n. R(l,w(i)))
(a,b,c:Alph*.
a':Alph*. ||a'|| < n
n & R((a @ b),a' @ b) & R((a @ c),a' @ c))
auto2_lemma_4
Thm* R:(Alph*Alph*Prop), n:.
(x:Alph*. R(x,x))
& (x,y:Alph*. R(x,y) R(y,x))
& (x,y,z:Alph*. R(x,y) & R(y,z) R(x,z))
& (x,y,z:Alph*. R(x,y) R((z @ x),z @ y))
& (w:(nAlph*). l:Alph*. i:n. R(l,w(i)))
(a,b,c:Alph*.
||a||
nn
(a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c)))
auto2_lemma_3
In prior sections: list 1 list 3 autom