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

At: sq stable is member 1 2
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)

SqStable(x(eq) (u.v))
By: Rewrite (HigherC is_member_unrollC) 0
Generated subgoal:

1 SqStable(if eq(x,u) true else x(eq) v fi)

About:
listconsboolbtrueifthenelseassertapplyfunctionuniverse

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