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)))))

About: