G:Grammar(V;T), l,m,n:(V+T)*. (l 
m) (m n) (l n)
derive_trans
(l,m)
== 
a:((V+T)* List
).
l = a[0] 
(V+T)* & (i:
(||a||-1). a[i] a[(i+1)]) & a[(||a||-1)] = m (V+T)*
Thm* G:Grammar(V;T), l,m,n:(V+T)*. (l m) (m n) (l n)
derive_trans
Thm* G:Grammar(V;T), l:(V+T)*. l l derive_refl