Nuprl - Pf formula_not_right

PrintForm Definitions elimination Sections ClassicalProps(jlc) Doc

hyp,M,N:Formula List, f:Formula, a:Assignment. a |= < f.hyp,M @ N > a |= < hyp,M @ (f.N) >

By: UnivCD THEN Analyze 0 THEN Analyze 0

Generated subgoals:

1 1. hyp: Formula List
2. M: Formula List
3. N: Formula List
4. f: Formula
5. a: Assignment
6. a |= < f.hyp,M @ N >
a |= < hyp,M @ (f.N) >

2 1. hyp: Formula List
2. M: Formula List
3. N: Formula List
4. f: Formula
5. a: Assignment
6. a |= < hyp,M @ (f.N) >
a |= < f.hyp,M @ N >

About:

1	1. `hyp:` `Formula List` 2. `M:` `Formula List` 3. `N:` `Formula List` 4. `f:` `Formula` 5. `a:` `Assignment` 6. `a \|= < f.hyp,M @ N >` `a \|= < hyp,M @ (f.N) >`
2	1. `hyp:` `Formula List` 2. `M:` `Formula List` 3. `N:` `Formula List` 4. `f:` `Formula` 5. `a:` `Assignment` 6. `a \|= < hyp,M @ (f.N) >` `a \|= < f.hyp,M @ N >`