Nuprl - Pf formula_or_right

1. hyp: Formula List
2. M: Formula List
3. N: Formula List
4. q: Formula
5. r: Formula
6. a: Full( < hyp,M @ (qr.N) > )

a |= < hyp,[q; r/ M @ N] > a | < hyp,[q; r/ M @ N] >

By: Analyze -1 THEN Analyze -1

Generated subgoals:

About:

1	6. `a:` `Assignment` 7. `a \|= < hyp,M @ (qr.N) >` `a \|= < hyp,[q; r/ M @ N] > a \| < hyp,[q; r/ M @ N] >`
2	6. `a:` `Assignment` 7. `a \| < hyp,M @ (qr.N) >` `a \|= < hyp,[q; r/ M @ N] > a \| < hyp,[q; r/ M @ N] >`