At:
l before-iff2122
1.
T: Type
2.
L: T List
3.
u: T
4.
v: T List
5.
x,y:T. x before y v (L1,L2,L3:T List. v = (L1 @ [x / (L2 @ [y / L3])]))
6.
x: T
7.
y: T
8.
u1: T
9.
v1: T List
10.
L2: T List
11.
L3: T List
12.
u = u1
13.
v = (v1 @ [x / (L2 @ [y / L3])])
x = u & (y v) x before y v
By:
OrRight
THEN
BackThruSomeHyp
Generated subgoal:
L1,L2,L3:T List. v = (L1 @ [x / (L2 @ [y / L3])])
x,y:T. x before y 
v 
(
x before y 
