Selected Objects
| def | Formula | Formula == rec(formula.Var+formula+(formula formula)+(formulaformula)+(formulaformula)) |
| def | formula_case | case F: x  varC(x); p1 notC(p1);p2 p3 andC(p2;p3);p4 p5 orC(p4;p5);p6  p7 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))))) |
| def | fvar | F == inl(F) |
| def | fnot | p == inr(inl(p)) |
| def | fand | pq == inr(inr(inl( < p,q > ))) |
| def | f_or | pq == inr(inr(inr(inl( < p,q > )))) |
| def | fimp | pq == inr(inr(inr(inr( < p,q > )))) |
| def | subformula | subformula(F) == case F:x nil;p [p];pq [p; q];pq [p; q];pq [p; q]; |