Nuprl - Pf formula_not_right

PrintForm Definitions elimination Sections ClassicalProps(jlc) Doc

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

a |= < hyp,M @ (f2.N) >

By: With a (Analyze -2)

Generated subgoals:

1 5. a: Full( < hyp,M @ (f2.N) > )
a Full( < f2.hyp,M @ N > )

2 5. a: Full( < hyp,M @ (f2.N) > )
6. a |= < f2.hyp,M @ N >
a |= < hyp,M @ (f2.N) >

About:

1	5. `a:` `Full( < hyp,M @ (f2.N) > )` `a Full( < f2.hyp,M @ N > )`
2	5. `a:` `Full( < hyp,M @ (f2.N) > )` 6. `a \|= < f2.hyp,M @ N >` `a \|= < hyp,M @ (f2.N) >`