1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/preamble".
17 include "../Base-1/definitions.ma".
20 cic:/Coq/Init/Logic/eq.ind
21 cic:/matita/LAMBDA-TYPES/Base-1/preamble/sym_eq.con
22 cic:/matita/LAMBDA-TYPES/Base-1/preamble/trans_eq.con
23 cic:/Coq/Init/Logic/eq_ind.con
24 cic:/Coq/Init/Logic/eq_ind_r.con
25 cic:/Coq/Init/Logic/eq_rec.con
26 cic:/Coq/Init/Logic/eq_rec_r.con
27 cic:/Coq/Init/Logic/eq_rect.con
28 cic:/Coq/Init/Logic/eq_rect_r.con
29 cic:/matita/LAMBDA-TYPES/Base-1/preamble/f_equal.con
30 cic:/matita/legacy/coq/f_equal1.con.