Nuprl - Pf formula_imp_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 |= < q.hyp,r.(M @ N) > a | < q.hyp,r.(M @ N) >

By: Analyze -1 THEN Analyze -1

Generated subgoals:

About:

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