Info: execution of auto.ma started: Debug: Executing: ``set "baseuri" "cic:/matita/tests/auto/"'' Debug: Executing: ``include cic:/matita/legacy/coq'' Debug: Executing: ``Theorem a: @[\forall ((x): (@[nat])).(\forall ((y) ...'' WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Datatypes/nat.ind WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/eq.ind WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/minus.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult.con Error: Bad name: a Debug: Executing: ``intro.'' Debug: Executing: ``auto.'' WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/trans_eq.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/z.var WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal3.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal2.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/B.var WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/f.var WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/add_sub_square_identity.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_Sm.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/semantics/conservation_0_0.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/technical_lemma.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/ARITH/Chinese/Nat_complements/technical_lemma.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/plus_minus.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus_simpl_l_reverse.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus.con WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_minus.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_r.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_plus_distr_r.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_plus_distr2.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_n.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_O.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/minus_minus_lem1.con WE HAVE NO UNIVERSE FILE FOR cic:/Cachan/SMC/mu/Splus_nm.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_Sm.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_Sn_m.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_Snm_nSm.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/bases/S_plus_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/mult_reg_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_reg_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute_2_in_4.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_comm.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc_reverse.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_r.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eq.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_permute2.con WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_eq_decompose.con WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/minus_decompose.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/minus_eq.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/eq_add_S.con WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/expand_mult2.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_2.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ring/ArithRing/S_to_plus_one.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ZArith/BinInt/ZL0.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/S_plus.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_n_SO.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_O.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_r.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Marseille/GC/lib_arith/lib_plus/plus_O_O.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eqO.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_O_O.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/plus_eqO.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/g0.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/McCarthy/g.var WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_SO.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/mult_SO.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack1.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ackermann/Ack.var WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_r.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult2_recompose.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_1.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_O.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_r.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_comm.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc_reverse.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc.con WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/square_recompose.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_sym.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_permut.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_assoc_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_r.con WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_l.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_eq.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_sym.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_permute.con WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Float/Faux/minus_inv_lt_aux.con WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_minus_distr_r.con WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult_minus_distr_l.con Error: Tactic error: No Applicable theorem