PrintForm Definitions elimination Sections ClassicalProps(jlc) Doc

At: formula or right sound 1 1 1

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 Full( < hyp,[q; r/ M @ N] > )

By: AbSetMemEqTypeCD

Generated subgoals:

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


About:
memberpairconslistor