At:
append paren
1
1.
T: Type
2.
u: T+T
3.
v: (T+T) List
4.
u1: T+T
5.
v1: (T+T) List
6.
paren(T;[u / v])
7.
paren(T;[u1 / v1])
paren(T;[u1 / v1] @ [u / v])
By:
RecUnfold `paren` 0
THEN
OrRight
THEN
OrRight
THEN
InstConcl [[u1 / v1];[u / v]]
THEN
Reduce 0
Generated subgoals:
None
About:
