(10steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

At: sq stable is member 1 2 1 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. eq(x,u) = true

SqStable(true)

By:
Rewrite (HigherC assert_evalC) 0
THEN
Unfold `sq_stable` 0
THEN
Unfold `squash` 0


Generated subgoals:

None

About:
listboolbtrueassertapplyfunctionuniverseequal

(10steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc