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. f: Formula
5. a: Assignment
6. a | f Fhyp.a | F FM.a |= F FN.a |= F

Fhyp.a | F FM.a |= F a |= f FN.a |= F

By: Analyze -1 THEN Analyze -1

Generated subgoals:

About:

1	6. `a \| f` `Fhyp.a \| F FM.a \|= F a \|= f FN.a \|= F`
2	6. `Fhyp.a \| F` `Fhyp.a \| F FM.a \|= F a \|= f FN.a \|= F`
3	6. `FM.a \|= F` `Fhyp.a \| F FM.a \|= F a \|= f FN.a \|= F`
4	6. `FN.a \|= F` `Fhyp.a \| F FM.a \|= F a \|= f FN.a \|= F`