Nuprl - Pf sq stable is member 1 2 1 1

1. T: Type
2. eq: TT
3. x: T
4. L: T List
5. u: T
6. v: T List
7. SqStable(x(eq) v)
8. b:
9. eq(x,u) = b

SqStable(if b true else x(eq) v fi)

By: BoolInd 8 THEN Rewrite (HigherC ifthenelse_evalC) 0

Generated subgoals:

1 8. eq(x,u) = true
SqStable(true)

2 8. eq(x,u) = false
SqStable(x(eq) v)

About:

1	8. `eq(x,u) = true` `SqStable(true)`
2	8. `eq(x,u) = false` `SqStable(x(eq) v)`