At: formula or left sound1121212 1. concl: Formula List 2. M: Formula List 3. N: Formula List 4. q: Formula 5. r: Formula 6. a: Full( < M @ (qr.N),concl > ) 7. F(M @ N).a | F 8. a | q
FM.a | F a | q & a | r FN.a | F Fconcl.a |= F By: FwdThru
Thm*P:(TProp), L,M:T List.
x(L @ M).P(x) xL.P(x) xM.P(x)
[-2] Generated subgoal: