Nuprl - Proof: l before decomp 2

1. T: Type
2. L: T List
3. x: T
4. y: T
5. A,B:T List. L = (A @ B) & (x A) & (y B)

x before y L

By: ExRepD THEN SubstFor L 0 THEN RWO Thm* A,B:T List, x,y:T. x before y A @ B x before y A x before y B (x A) & (y B) 0 THEN OrRight THEN OrRight

Generated subgoals:

None

About: