F
p
q
q
q
x:A. B(x)x 
varC(x);p1 notC(p1);p2p3 andC(p2;p3);p4p5 orC(p4;p5);p6p7 impC(p6;p7);
| Def | F | [fvar] | ||
| Def | p | [fnot] | ||
| Def | pq | [fand] | ||
| Def | pq | [f_or] | ||
| Def | pq | [fimp] | ||
| Def | subformula(F) | [subformula] | ||
| Def | Formula | [Formula] | ||
| Def | x:A. B(x) | [all] | core | |
| Def | Var | [Var] | var jlc | |
| Def | case F:x varC(x);p1 notC(p1);p2p3 andC(p2;p3);p4p5 orC(p4;p5);p6p7 impC(p6;p7); | [formula_case] |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |