1 <?xml version="1.0" encoding="utf-8"?>
3 <section name="matex.alpha">
4 <key name="type">matita.lambdadelta.basic_1.T.defs.B.B.type b I</key>
5 <key name="type">matita.lambdadelta.basic_1.T.defs.B.B.type ee I</key>
6 <key name="type">matita.lambdadelta.basic_1.T.defs.B.B.type x I</key>
8 <key name="type">matita.lambdadelta.basic_1.T.defs.F.F.type ee I</key>
9 <key name="type">matita.lambdadelta.basic_1.T.defs.F.F.type f I</key>
10 <key name="type">matita.lambdadelta.basic_1.T.defs.F.F.type x I</key>
12 <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type e I</key>
13 <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type ee I</key>
14 <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type k I</key>
15 <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type h I</key>
16 <key name="type">matita.lambdadelta.basic_1.T.defs.K.K.type x I</key>
18 <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type _ X</key>
19 <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type a X</key>
20 <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type c L</key>
21 <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type d L</key>
22 <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type e K</key>
23 <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type ee X</key>
24 <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type x X</key>
25 <key name="type">matita.lambdadelta.basic_1.C.defs.C.C.type y Y</key>
27 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type _ X</key>
28 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type e X</key>
29 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type ee X</key>
30 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type t T</key>
31 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type u U</key>
32 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type v V</key>
33 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type w W</key>
34 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type wi W</key>
35 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type x X</key>
36 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type y Y</key>
37 <key name="type">matita.lambdadelta.basic_1.T.defs.T.T.type z Z</key>
39 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type _ Xs</key>
40 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type e Xs</key>
41 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ee Xs</key>
42 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type t Ts</key>
43 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ts Ts</key>
44 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ul Us</key>
45 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type us Us</key>
46 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type vs Vs</key>
47 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ws Ws</key>
48 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type xs Xs</key>
49 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type x Xs</key>
50 <key name="type">matita.lambdadelta.basic_1.tlist.defs.TList.TList.type y Ys</key>
52 <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type _ X</key>
53 <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type a A</key>
54 <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type b B</key>
55 <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type e X</key>
56 <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type ee X</key>
57 <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type l X</key>
58 <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type x X</key>
59 <key name="type">matita.lambdadelta.basic_1.A.defs.A.A.type y Y</key>
61 <key name="type">matita.lambdadelta.basic_1.G.defs.G.G.type g h</key>
63 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type _ x</key>
64 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d' d</key>
65 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d d</key>
66 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type e e</key>
67 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type ee e</key>
68 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type f f</key>
69 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type g g</key>
70 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type h h</key>
71 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type i i</key>
72 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type j j</key>
73 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type k k</key>
74 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type l l</key>
75 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type m m</key>
76 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type n n</key>
77 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type next f</key>
78 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type v v</key>
79 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type w w</key>
80 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type x x</key>
81 <key name="type">matita.lambdadelta.legacy_1.coq.defs.nat.nat.type y y</key>
83 <key name="type">matita.lambdadelta.legacy_1.coq.defs.bool.bool.type b b</key>
84 <key name="type">matita.lambdadelta.legacy_1.coq.defs.bool.bool.type x x</key>
86 <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type _ f</key>
87 <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type e f</key>
88 <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type ee f</key>
89 <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type hds f</key>
90 <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type is f</key>
91 <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type p f</key>
92 <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type q f</key>
93 <key name="type">matita.lambdadelta.ground_1.plist.defs.PList.PList.type y f</key>
95 <key name="type">Prop P R</key>
96 <key name="type">Prop Q R</key>
98 <key name="type">Type[cic:/matita/pts/Type0.univ] P S</key>
100 <key name="sort">Prop H H</key>
101 <key name="sort">Prop Hle H</key>
102 <key name="sort">Prop IH IH</key>
103 <key name="sort">Prop IHc IH</key>
104 <key name="sort">Prop IHd IH</key>
105 <key name="sort">Prop IHe IH</key>
106 <key name="sort">Prop IHh IH</key>
107 <key name="sort">Prop IHi IH</key>
108 <key name="sort">Prop IHj IH</key>
109 <key name="sort">Prop IHn IH</key>
110 <key name="sort">Prop IHx IH</key>
111 <key name="sort">Prop a H</key>
112 <key name="sort">Prop c H</key>
113 <key name="sort">Prop d H</key>
114 <key name="sort">Prop e H</key>
115 <key name="sort">Prop f H</key>
116 <key name="sort">Prop g H</key>
117 <key name="sort">Prop h H</key>
118 <key name="sort">Prop i H</key>
119 <key name="sort">Prop l H</key>
120 <key name="sort">Prop n H</key>
121 <key name="sort">Prop p H</key>
122 <key name="sort">Prop s H</key>
123 <key name="sort">Prop t H</key>
124 <key name="sort">Prop w H</key>
125 <key name="sort">Prop x H</key>
127 <key name="sort">Type[cic:/matita/pts/Type0.univ] f a</key>
129 <key name="gref">clt_wf__q_ind q_ind_aux</key>
131 <key name="gref">ex1__leq_sort_SS leq_sort_SS_aux</key>
133 <key name="gref">flt_wf__q_ind q_ind_aux</key>
135 <key name="gref">llt_wf__q_ind q_ind_aux</key>
137 <key name="gref">nf2_gen__nf2_gen_aux nf2_gen_aux</key>
139 <key name="gref">pc3_ind_left__pc3_left_pc3 pc3_left_pc3_aux</key>
140 <key name="gref">pc3_ind_left__pc3_left_pr3 pc3_left_pr3_aux</key>
141 <key name="gref">pc3_ind_left__pc3_left_sym pc3_left_sym_aux</key>
142 <key name="gref">pc3_ind_left__pc3_left_trans pc3_left_trans_aux</key>
143 <key name="gref">pc3_ind_left__pc3_pc3_left pc3_pc3_left_aux</key>
144 <key name="gref">pc3_wcpr0__pc3_wcpr0_t_aux pc3_wcpr0_t_aux</key>
146 <key name="gref">pr0_confluence__pr0_cong_delta pr0_cong_delta_aux</key>
147 <key name="gref">pr0_confluence__pr0_cong_upsilon_cong pr0_cong_upsilon_cong_aux</key>
148 <key name="gref">pr0_confluence__pr0_cong_upsilon_delta pr0_cong_upsilon_delta_aux</key>
149 <key name="gref">pr0_confluence__pr0_cong_upsilon_refl pr0_cong_upsilon_refl_aux</key>
150 <key name="gref">pr0_confluence__pr0_cong_upsilon_zeta pr0_cong_upsilon_zeta_aux</key>
151 <key name="gref">pr0_confluence__pr0_delta_delta pr0_delta_delta_aux</key>
152 <key name="gref">pr0_confluence__pr0_delta_tau pr0_delta_tau_aux</key>
153 <key name="gref">pr0_confluence__pr0_upsilon_upsilon pr0_upsilon_upsilon_aux</key>
155 <key name="gref">pr2_confluence__pr2_delta_delta pr2_delta_delta_aux</key>
156 <key name="gref">pr2_confluence__pr2_free_delta pr2_free_delta_aux</key>
157 <key name="gref">pr2_confluence__pr2_free_free pr2_free_free_aux</key>
159 <key name="gref">sc3_props__sc3_sn3_abst sc3_sn3_abst_aux</key>
161 <key name="gref">terms_props__bind_dec bind_dec_aux</key>
162 <key name="gref">terms_props__flat_dec flat_dec_aux</key>
163 <key name="gref">terms_props__kind_dec kind_dec_aux</key>
165 <key name="gref">tlt_wf__q_ind q_ind_aux</key>
166 <key name="gref">tslt_wf__q_ind q_ind_aux</key>
167 <key name="gref">ty3_nf2_gen__ty3_nf2_inv_abst_aux ty3_nf2_inv_abst_aux</key>
171 matita.lambdadelta.basic_1.A.defs.A.AHead.type
172 matita.lambdadelta.basic_1.A.defs.A.ASort.type
173 matita.lambdadelta.basic_1.A.fwd.A_rect.A_rect.type
174 matita.lambdadelta.basic_1.aplus.defs.aplus.aplus.type
175 matita.lambdadelta.basic_1.app.defs.app1.app1.type
176 matita.lambdadelta.basic_1.app.defs.cbk.cbk.type
177 matita.lambdadelta.basic_1.aprem.defs.aprem.aprem.type
178 matita.lambdadelta.basic_1.arity.defs.arity.arity.type
179 matita.lambdadelta.basic_1.asucc.defs.asucc.asucc.type
180 matita.lambdadelta.basic_1.C.defs.C.CHead.type
181 matita.lambdadelta.basic_1.C.defs.C.CSort.type
182 matita.lambdadelta.basic_1.C.defs.cle.type
183 matita.lambdadelta.basic_1.C.defs.clt.type
184 matita.lambdadelta.basic_1.C.defs.CTail.CTail.type
185 matita.lambdadelta.basic_1.C.defs.cweight.cweight.type
186 matita.lambdadelta.basic_1.C.fwd.C_rect.C_rect.type
187 matita.lambdadelta.basic_1.cimp.defs.cimp.type
188 matita.lambdadelta.basic_1.clear.defs.clear.clear.type
189 matita.lambdadelta.basic_1.clen.defs.clen.clen.type
190 matita.lambdadelta.basic_1.cnt.defs.cnt.cnt.type
191 matita.lambdadelta.basic_1.csuba.defs.csuba.csuba.type
192 matita.lambdadelta.basic_1.csubc.defs.csubc.csubc.type
193 matita.lambdadelta.basic_1.csubst0.defs.csubst0.csubst0.type
194 matita.lambdadelta.basic_1.csubst1.defs.csubst1.csubst1.type
195 matita.lambdadelta.basic_1.csubt.defs.csubt.csubt.type
196 matita.lambdadelta.basic_1.csubv.defs.csubv.csubv.type
197 matita.lambdadelta.basic_1.drop1.defs.drop1.drop1.type
198 matita.lambdadelta.basic_1.drop1.defs.ptrans.ptrans.type
199 matita.lambdadelta.basic_1.drop.defs.drop.drop.type
200 matita.lambdadelta.basic_1.ex0.defs.leqz.leqz.type
201 matita.lambdadelta.basic_1.flt.defs.flt.type
202 matita.lambdadelta.basic_1.flt.defs.fweight.type
203 matita.lambdadelta.basic_1.fsubst0.defs.fsubst0.fsubst0.type
204 matita.lambdadelta.basic_1.G.defs.G.mk_G.type
205 matita.lambdadelta.basic_1.G.defs.next.next.type
206 matita.lambdadelta.basic_1.getl.defs.getl.getl.type
207 matita.lambdadelta.basic_1.iso.defs.iso.iso.type
208 matita.lambdadelta.basic_1.leq.defs.leq.leq.type
209 matita.lambdadelta.basic_1.lift1.defs.lift1.lift1.type
210 matita.lambdadelta.basic_1.lift1.defs.lifts1.lifts1.type
211 matita.lambdadelta.basic_1.lift1.defs.trans.trans.type
212 matita.lambdadelta.basic_1.lift.defs.lifts.lifts.type
213 matita.lambdadelta.basic_1.lift.defs.lift.type
214 matita.lambdadelta.basic_1.lift.defs.lref_map.lref_map.type
215 matita.lambdadelta.basic_1.llt.defs.llt.type
216 matita.lambdadelta.basic_1.llt.defs.lweight.lweight.type
217 matita.lambdadelta.basic_1.next_plus.defs.next_plus.next_plus.type
218 matita.lambdadelta.basic_1.nf2.defs.nf2.type
219 matita.lambdadelta.basic_1.nf2.defs.nfs2.nfs2.type
220 matita.lambdadelta.basic_1.pc1.defs.pc1.type
221 matita.lambdadelta.basic_1.pc3.defs.pc3_left.pc3_left.type
222 matita.lambdadelta.basic_1.pc3.defs.pc3.type
223 matita.lambdadelta.basic_1.pr0.defs.pr0.pr0.type
224 matita.lambdadelta.basic_1.pr1.defs.pr1.pr1.type
225 matita.lambdadelta.basic_1.pr2.defs.pr2.pr2.type
226 matita.lambdadelta.basic_1.pr3.defs.pr3.pr3.type
227 matita.lambdadelta.basic_1.r.defs.r.type
228 matita.lambdadelta.basic_1.sc3.defs.sc3.sc3.type
229 matita.lambdadelta.basic_1.s.defs.s.type
230 matita.lambdadelta.basic_1.sn3.defs.sn3.sn3.type
231 matita.lambdadelta.basic_1.sn3.defs.sns3.sns3.type
232 matita.lambdadelta.basic_1.sty0.defs.sty0.sty0.type
233 matita.lambdadelta.basic_1.sty1.defs.sty1.sty1.type
234 matita.lambdadelta.basic_1.subst0.defs.subst0.subst0.type
235 matita.lambdadelta.basic_1.subst1.defs.subst1.subst1.type
236 matita.lambdadelta.basic_1.subst.defs.subst.subst.type
237 matita.lambdadelta.basic_1.T.defs.K.Bind.type
238 matita.lambdadelta.basic_1.T.defs.K.Flat.type
239 matita.lambdadelta.basic_1.T.defs.tle.type
240 matita.lambdadelta.basic_1.T.defs.T.THead.type
241 matita.lambdadelta.basic_1.T.defs.T.TLRef.type
242 matita.lambdadelta.basic_1.T.defs.T.TSort.type
243 matita.lambdadelta.basic_1.T.defs.tweight.tweight.type
244 matita.lambdadelta.basic_1.T.fwd.T_rect.T_rect.type
245 matita.lambdadelta.basic_1.tlist.defs.TApp.TApp.type
246 matita.lambdadelta.basic_1.tlist.defs.THeads.THeads.type
247 matita.lambdadelta.basic_1.tlist.defs.TList.TCons.type
248 matita.lambdadelta.basic_1.tlist.defs.tslen.tslen.type
249 matita.lambdadelta.basic_1.tlist.defs.tslt.type
250 matita.lambdadelta.basic_1.tlt.defs.tlt.type
251 matita.lambdadelta.basic_1.tlt.defs.wadd.type
252 matita.lambdadelta.basic_1.tlt.defs.weight_map.weight_map.type
253 matita.lambdadelta.basic_1.tlt.defs.weight.type
254 matita.lambdadelta.basic_1.ty3.defs.ty3.ty3.type
255 matita.lambdadelta.basic_1.ty3.defs.tys3.tys3.type
256 matita.lambdadelta.basic_1.ty3.nf2.ty3_nf2_inv_abst_premise.type
257 matita.lambdadelta.basic_1.wcpr0.defs.wcpr0.wcpr0.type
258 matita.lambdadelta.basic_1.wf3.defs.wf3.wf3.type