Who Cites Formula?
Formula	Def Formula == rec(formula.Var+formula+(formulaformula)+(formulaformula)+(formulaformula))
	Thm* Formula Type
subformula	Def subformula(F) == case F:x nil;p [p];pq [p; q];pq [p; q];pq [p; q];
	Thm* F:Formula. subformula(F) Formula List
formula_case	Def case F: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)))))
Var	Def Var == Atom
	Thm* Var Type

About: