Nuprl - Pf sublist iff assert sublist 2 x 1

1. T: Type
2. L: T List
3. M: T List
4. eq: {T=}

L(eq)M (eq)(L,M)

By: Analyze 2 THEN Rewrite (HigherC sublist_unrollC THENC HigherC sublist_2_unrollC THENC TryC (HigherC assert_evalC)) 0

Generated subgoals:

1 True True

2 5. u: T
6. v: T List
u(eq) M & v(eq)M (u(eq) Mxv.x(eq) M)

About:

1	`True True`
2	5. `u:` `T` 6. `v:` `T List` `u(eq) M & v(eq)M (u(eq) Mxv.x(eq) M)`