(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/propositional_sequent_calculus/".
-
include "nat/plus.ma".
include "nat/compare.ma".
include "list/sort.ma".
simplify;
apply (ex_intro ? ? a3);
apply (ex_intro ? ? a4);
- autobatch
+ autobatch depth=4
| right;
intro;
apply (bool_elim ? (same_atom a (FAtom n1)));