x
nil;
p [p];p
q [p; q];p
q [p; q];p
q [p; q];x varC(x);p1 notC(p1);p2p3 andC(p2;p3);p4p5 orC(p4;p5);p6p7 impC(p6;p7); == InjCase(F; x. varC(x); F. InjCase(F; p1. notC(p1); F. InjCase(F; x. x/p2,p3. andC(p2;p3); F. InjCase(F; x. x/p4,p5. orC(p4;p5), x/p6,p7. impC(p6;p7)))))
is mentioned by
| Def subformula(F) == case F:x nil;p [p];pq [p; q];pq [p; q];pq [p; q]; | [subformula] |
Try larger context:
ClassicalProps(jlc)