At: lang prod functionality 1
1. Alph: Type
2. L: Alph*![](FONT/dash.png)
Prop
3. L': Alph*![](FONT/dash.png)
Prop
4. M: Alph*![](FONT/dash.png)
Prop
5. M': Alph*![](FONT/dash.png)
Prop
6.
l:Alph*. L(l) ![](FONT/if_big.png)
L'(l)
7.
l:Alph*. M(l) ![](FONT/if_big.png)
M'(l)
8. l: Alph*
(
i:{0...||l||}. L(l[0..i
]) & M(l[i..||l||
])) ![](FONT/if_big.png)
(
i:{0...||l||}. L'(l[0..i
]) & M'(l[i..||l||
]))
By:
RWH (HypC 6) 0
THEN
RWH (HypC 7) 0
Generated subgoals:None
About: