Nuprl - Pf back_listify 1 1 1

1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. Fin(Alph)
5. Fin(S.car)
6. LL: (S.carS.car*)*

BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:||nil||. 1of(nil[i]) = t & mem_f(S.car;s;2of(nil[i])))

By: Reduce 0 THEN InstConcl [nil] THEN Reduce 0

Generated subgoal:

1 7. t: S.car
8. i:0. 1of(nil[i]) = t & mem_f(S.car;s;2of(nil[i]))
False

About: