T+T 
(inl(i) s') inl(i) = inr(t) T+T
inr(i) = inl(t) T+T (inr(i) s') inr(i) = inr(t) T+T
i:T. (inl(i) s') 
(inr(i) s')
[inl(t)] @ s' @ [inr(t)])
(inr(i) [inl(t)] @ s' @ [inr(t)])
i.
(RWW
Thm* x:T, l1,l2:T List. (x l1 @ l2) 
(x l1) (x l2)
i)
THEN
(RWO
Thm* a,x:T. (x [a]) x = a
i))
| 1 | 7. inl(i) = inl(t) T+T (inl(i) s') inl(i) = inr(t) T+T inr(i) = inl(t) T+T (inr(i) s') inr(i) = inr(t) T+T | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |  |