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 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Logic_Type.v,v 1.19.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
36 Set Implicit Arguments.
39 (*#* This module defines quantification on the world [Type]
40 ([Logic.v] was defining it on the world [Set]) *)
42 include "Init/Datatypes.ma".
44 include "Init/Logic.ma".
46 inline procedural "cic:/Coq/Init/Logic_Type/notT.con" as definition.
49 Section identity_is_a_congruence
53 cic:/Coq/Init/Logic_Type/identity_is_a_congruence/A.var
57 cic:/Coq/Init/Logic_Type/identity_is_a_congruence/B.var
61 cic:/Coq/Init/Logic_Type/identity_is_a_congruence/f.var
65 cic:/Coq/Init/Logic_Type/identity_is_a_congruence/x.var
69 cic:/Coq/Init/Logic_Type/identity_is_a_congruence/y.var
73 cic:/Coq/Init/Logic_Type/identity_is_a_congruence/z.var
76 inline procedural "cic:/Coq/Init/Logic_Type/sym_id.con" as lemma.
78 inline procedural "cic:/Coq/Init/Logic_Type/trans_id.con" as lemma.
80 inline procedural "cic:/Coq/Init/Logic_Type/congr_id.con" as lemma.
82 inline procedural "cic:/Coq/Init/Logic_Type/sym_not_id.con" as lemma.
85 End identity_is_a_congruence
88 inline procedural "cic:/Coq/Init/Logic_Type/identity_ind_r.con" as definition.
90 inline procedural "cic:/Coq/Init/Logic_Type/identity_rec_r.con" as definition.
92 inline procedural "cic:/Coq/Init/Logic_Type/identity_rect_r.con" as definition.
94 inline procedural "cic:/Coq/Init/Logic_Type/prodT.ind".
101 cic:/Coq/Init/Logic_Type/prodT_proj/A.var
105 cic:/Coq/Init/Logic_Type/prodT_proj/B.var
108 inline procedural "cic:/Coq/Init/Logic_Type/fstT.con" as definition.
110 inline procedural "cic:/Coq/Init/Logic_Type/sndT.con" as definition.
116 inline procedural "cic:/Coq/Init/Logic_Type/prodT_uncurry.con" as definition.
118 inline procedural "cic:/Coq/Init/Logic_Type/prodT_curry.con" as definition.
121 Hint Immediate sym_id sym_not_id: core v62.