Nuprl - Pf list exists append lemma

(35steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

T:Type, P:(TProp), L,M:T List. x(L @ M).P(x) xL.P(x) xM.P(x)

By: UnivCD THEN Repeat (Analyze 0)

Generated subgoals:

1 1. T: Type
2. P: TProp
3. L: T List
4. M: T List
5. x(L @ M).P(x)
xL.P(x) xM.P(x)

2 1. T: Type
2. P: TProp
3. L: T List
4. M: T List
5. xL.P(x) xM.P(x)
x(L @ M).P(x)

About:

(35steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

1	1. `T:` `Type` 2. `P:` `TProp` 3. `L:` `T List` 4. `M:` `T List` 5. `x(L @ M).P(x)` `xL.P(x) xM.P(x)`
2	1. `T:` `Type` 2. `P:` `TProp` 3. `L:` `T List` 4. `M:` `T List` 5. `xL.P(x) xM.P(x)` `x(L @ M).P(x)`