At:
sq stable is member
1
2
1
1
1
1.
T: Type
2.
eq: T
T
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:
