10. x1: Alph*
11. x2: Alph*
12. x1 R x2
(a.x1) R (a.x2)
Alph*Prop
x,y,z:Alph*. (x R y) 
((z @ x) R (z @ y))
(x,y:Alph*//(x R y))) a:Alph, x:x,y:Alph*//(x R y). a.x 
x,y:Alph*//(x R y)| 1 | 9. a: Alph 10. x1: Alph* 11. x2: Alph* 12. x1 R x2 (a.x1) R (a.x2) |
About:
 |  |  |  |  |  |
 |  |  |  |  |