-
Notifications
You must be signed in to change notification settings - Fork 2
/
syntax.v
423 lines (317 loc) · 29.6 KB
/
syntax.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
Require Export unscoped.
Section tm.
Inductive tm : Type :=
| var_tm : ( fin ) -> tm
| tAbs : ( tm ) -> tm
| tApp : ( tm ) -> ( tm ) -> tm
| tPi : ( tm ) -> ( tm ) -> tm
| tUniv : ( nat ) -> tm
| tEq : ( tm ) -> ( tm ) -> ( tm ) -> tm
| tJ : ( tm ) -> ( tm ) -> ( tm ) -> ( tm ) -> tm
| tRefl : tm
| tZero : tm
| tSuc : ( tm ) -> tm
| tInd : ( tm ) -> ( tm ) -> ( tm ) -> tm
| tNat : tm
| tSig : ( tm ) -> ( tm ) -> tm
| tPack : ( tm ) -> ( tm ) -> tm
| tLet : ( tm ) -> ( tm ) -> tm .
Lemma congr_tAbs { s0 : tm } { t0 : tm } (H1 : s0 = t0) : tAbs s0 = tAbs t0 .
Proof. congruence. Qed.
Lemma congr_tApp { s0 : tm } { s1 : tm } { t0 : tm } { t1 : tm } (H1 : s0 = t0) (H2 : s1 = t1) : tApp s0 s1 = tApp t0 t1 .
Proof. congruence. Qed.
Lemma congr_tPi { s0 : tm } { s1 : tm } { t0 : tm } { t1 : tm } (H1 : s0 = t0) (H2 : s1 = t1) : tPi s0 s1 = tPi t0 t1 .
Proof. congruence. Qed.
Lemma congr_tUniv { s0 : nat } { t0 : nat } (H1 : s0 = t0) : tUniv s0 = tUniv t0 .
Proof. congruence. Qed.
Lemma congr_tEq { s0 : tm } { s1 : tm } { s2 : tm } { t0 : tm } { t1 : tm } { t2 : tm } (H1 : s0 = t0) (H2 : s1 = t1) (H3 : s2 = t2) : tEq s0 s1 s2 = tEq t0 t1 t2 .
Proof. congruence. Qed.
Lemma congr_tJ { s0 : tm } { s1 : tm } { s2 : tm } { s3 : tm } { t0 : tm } { t1 : tm } { t2 : tm } { t3 : tm } (H1 : s0 = t0) (H2 : s1 = t1) (H3 : s2 = t2) (H4 : s3 = t3) : tJ s0 s1 s2 s3 = tJ t0 t1 t2 t3 .
Proof. congruence. Qed.
Lemma congr_tRefl : tRefl = tRefl .
Proof. congruence. Qed.
Lemma congr_tZero : tZero = tZero .
Proof. congruence. Qed.
Lemma congr_tSuc { s0 : tm } { t0 : tm } (H1 : s0 = t0) : tSuc s0 = tSuc t0 .
Proof. congruence. Qed.
Lemma congr_tInd { s0 : tm } { s1 : tm } { s2 : tm } { t0 : tm } { t1 : tm } { t2 : tm } (H1 : s0 = t0) (H2 : s1 = t1) (H3 : s2 = t2) : tInd s0 s1 s2 = tInd t0 t1 t2 .
Proof. congruence. Qed.
Lemma congr_tNat : tNat = tNat .
Proof. congruence. Qed.
Lemma congr_tSig { s0 : tm } { s1 : tm } { t0 : tm } { t1 : tm } (H1 : s0 = t0) (H2 : s1 = t1) : tSig s0 s1 = tSig t0 t1 .
Proof. congruence. Qed.
Lemma congr_tPack { s0 : tm } { s1 : tm } { t0 : tm } { t1 : tm } (H1 : s0 = t0) (H2 : s1 = t1) : tPack s0 s1 = tPack t0 t1 .
Proof. congruence. Qed.
Lemma congr_tLet { s0 : tm } { s1 : tm } { t0 : tm } { t1 : tm } (H1 : s0 = t0) (H2 : s1 = t1) : tLet s0 s1 = tLet t0 t1 .
Proof. congruence. Qed.
Definition upRen_tm_tm (xi : ( fin ) -> fin) : ( fin ) -> fin :=
(up_ren) xi.
Fixpoint ren_tm (xitm : ( fin ) -> fin) (s : tm ) : tm :=
match s return tm with
| var_tm s => (var_tm ) (xitm s)
| tAbs s0 => tAbs ((ren_tm (upRen_tm_tm xitm)) s0)
| tApp s0 s1 => tApp ((ren_tm xitm) s0) ((ren_tm xitm) s1)
| tPi s0 s1 => tPi ((ren_tm xitm) s0) ((ren_tm (upRen_tm_tm xitm)) s1)
| tUniv s0 => tUniv ((fun x => x) s0)
| tEq s0 s1 s2 => tEq ((ren_tm xitm) s0) ((ren_tm xitm) s1) ((ren_tm xitm) s2)
| tJ s0 s1 s2 s3 => tJ ((ren_tm xitm) s0) ((ren_tm xitm) s1) ((ren_tm xitm) s2) ((ren_tm xitm) s3)
| tRefl => tRefl
| tZero => tZero
| tSuc s0 => tSuc ((ren_tm xitm) s0)
| tInd s0 s1 s2 => tInd ((ren_tm xitm) s0) ((ren_tm (upRen_tm_tm (upRen_tm_tm xitm))) s1) ((ren_tm xitm) s2)
| tNat => tNat
| tSig s0 s1 => tSig ((ren_tm xitm) s0) ((ren_tm (upRen_tm_tm xitm)) s1)
| tPack s0 s1 => tPack ((ren_tm xitm) s0) ((ren_tm xitm) s1)
| tLet s0 s1 => tLet ((ren_tm xitm) s0) ((ren_tm (upRen_tm_tm (upRen_tm_tm xitm))) s1)
end.
Definition up_tm_tm (sigma : ( fin ) -> tm ) : ( fin ) -> tm :=
(scons) ((var_tm ) (var_zero)) ((funcomp) (ren_tm (shift)) sigma).
Fixpoint subst_tm (sigmatm : ( fin ) -> tm ) (s : tm ) : tm :=
match s return tm with
| var_tm s => sigmatm s
| tAbs s0 => tAbs ((subst_tm (up_tm_tm sigmatm)) s0)
| tApp s0 s1 => tApp ((subst_tm sigmatm) s0) ((subst_tm sigmatm) s1)
| tPi s0 s1 => tPi ((subst_tm sigmatm) s0) ((subst_tm (up_tm_tm sigmatm)) s1)
| tUniv s0 => tUniv ((fun x => x) s0)
| tEq s0 s1 s2 => tEq ((subst_tm sigmatm) s0) ((subst_tm sigmatm) s1) ((subst_tm sigmatm) s2)
| tJ s0 s1 s2 s3 => tJ ((subst_tm sigmatm) s0) ((subst_tm sigmatm) s1) ((subst_tm sigmatm) s2) ((subst_tm sigmatm) s3)
| tRefl => tRefl
| tZero => tZero
| tSuc s0 => tSuc ((subst_tm sigmatm) s0)
| tInd s0 s1 s2 => tInd ((subst_tm sigmatm) s0) ((subst_tm (up_tm_tm (up_tm_tm sigmatm))) s1) ((subst_tm sigmatm) s2)
| tNat => tNat
| tSig s0 s1 => tSig ((subst_tm sigmatm) s0) ((subst_tm (up_tm_tm sigmatm)) s1)
| tPack s0 s1 => tPack ((subst_tm sigmatm) s0) ((subst_tm sigmatm) s1)
| tLet s0 s1 => tLet ((subst_tm sigmatm) s0) ((subst_tm (up_tm_tm (up_tm_tm sigmatm))) s1)
end.
Definition upId_tm_tm (sigma : ( fin ) -> tm ) (Eq : forall x, sigma x = (var_tm ) x) : forall x, (up_tm_tm sigma) x = (var_tm ) x :=
fun n => match n with
| S fin_n => (ap) (ren_tm (shift)) (Eq fin_n)
| 0 => eq_refl
end.
Fixpoint idSubst_tm (sigmatm : ( fin ) -> tm ) (Eqtm : forall x, sigmatm x = (var_tm ) x) (s : tm ) : subst_tm sigmatm s = s :=
match s return subst_tm sigmatm s = s with
| var_tm s => Eqtm s
| tAbs s0 => congr_tAbs ((idSubst_tm (up_tm_tm sigmatm) (upId_tm_tm (_) Eqtm)) s0)
| tApp s0 s1 => congr_tApp ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm sigmatm Eqtm) s1)
| tPi s0 s1 => congr_tPi ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm (up_tm_tm sigmatm) (upId_tm_tm (_) Eqtm)) s1)
| tUniv s0 => congr_tUniv ((fun x => (eq_refl) x) s0)
| tEq s0 s1 s2 => congr_tEq ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm sigmatm Eqtm) s1) ((idSubst_tm sigmatm Eqtm) s2)
| tJ s0 s1 s2 s3 => congr_tJ ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm sigmatm Eqtm) s1) ((idSubst_tm sigmatm Eqtm) s2) ((idSubst_tm sigmatm Eqtm) s3)
| tRefl => congr_tRefl
| tZero => congr_tZero
| tSuc s0 => congr_tSuc ((idSubst_tm sigmatm Eqtm) s0)
| tInd s0 s1 s2 => congr_tInd ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm (up_tm_tm (up_tm_tm sigmatm)) (upId_tm_tm (_) (upId_tm_tm (_) Eqtm))) s1) ((idSubst_tm sigmatm Eqtm) s2)
| tNat => congr_tNat
| tSig s0 s1 => congr_tSig ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm (up_tm_tm sigmatm) (upId_tm_tm (_) Eqtm)) s1)
| tPack s0 s1 => congr_tPack ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm sigmatm Eqtm) s1)
| tLet s0 s1 => congr_tLet ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm (up_tm_tm (up_tm_tm sigmatm)) (upId_tm_tm (_) (upId_tm_tm (_) Eqtm))) s1)
end.
Definition upExtRen_tm_tm (xi : ( fin ) -> fin) (zeta : ( fin ) -> fin) (Eq : forall x, xi x = zeta x) : forall x, (upRen_tm_tm xi) x = (upRen_tm_tm zeta) x :=
fun n => match n with
| S fin_n => (ap) (shift) (Eq fin_n)
| 0 => eq_refl
end.
Fixpoint extRen_tm (xitm : ( fin ) -> fin) (zetatm : ( fin ) -> fin) (Eqtm : forall x, xitm x = zetatm x) (s : tm ) : ren_tm xitm s = ren_tm zetatm s :=
match s return ren_tm xitm s = ren_tm zetatm s with
| var_tm s => (ap) (var_tm ) (Eqtm s)
| tAbs s0 => congr_tAbs ((extRen_tm (upRen_tm_tm xitm) (upRen_tm_tm zetatm) (upExtRen_tm_tm (_) (_) Eqtm)) s0)
| tApp s0 s1 => congr_tApp ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm xitm zetatm Eqtm) s1)
| tPi s0 s1 => congr_tPi ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm (upRen_tm_tm xitm) (upRen_tm_tm zetatm) (upExtRen_tm_tm (_) (_) Eqtm)) s1)
| tUniv s0 => congr_tUniv ((fun x => (eq_refl) x) s0)
| tEq s0 s1 s2 => congr_tEq ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm xitm zetatm Eqtm) s1) ((extRen_tm xitm zetatm Eqtm) s2)
| tJ s0 s1 s2 s3 => congr_tJ ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm xitm zetatm Eqtm) s1) ((extRen_tm xitm zetatm Eqtm) s2) ((extRen_tm xitm zetatm Eqtm) s3)
| tRefl => congr_tRefl
| tZero => congr_tZero
| tSuc s0 => congr_tSuc ((extRen_tm xitm zetatm Eqtm) s0)
| tInd s0 s1 s2 => congr_tInd ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm (upRen_tm_tm (upRen_tm_tm xitm)) (upRen_tm_tm (upRen_tm_tm zetatm)) (upExtRen_tm_tm (_) (_) (upExtRen_tm_tm (_) (_) Eqtm))) s1) ((extRen_tm xitm zetatm Eqtm) s2)
| tNat => congr_tNat
| tSig s0 s1 => congr_tSig ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm (upRen_tm_tm xitm) (upRen_tm_tm zetatm) (upExtRen_tm_tm (_) (_) Eqtm)) s1)
| tPack s0 s1 => congr_tPack ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm xitm zetatm Eqtm) s1)
| tLet s0 s1 => congr_tLet ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm (upRen_tm_tm (upRen_tm_tm xitm)) (upRen_tm_tm (upRen_tm_tm zetatm)) (upExtRen_tm_tm (_) (_) (upExtRen_tm_tm (_) (_) Eqtm))) s1)
end.
Definition upExt_tm_tm (sigma : ( fin ) -> tm ) (tau : ( fin ) -> tm ) (Eq : forall x, sigma x = tau x) : forall x, (up_tm_tm sigma) x = (up_tm_tm tau) x :=
fun n => match n with
| S fin_n => (ap) (ren_tm (shift)) (Eq fin_n)
| 0 => eq_refl
end.
Fixpoint ext_tm (sigmatm : ( fin ) -> tm ) (tautm : ( fin ) -> tm ) (Eqtm : forall x, sigmatm x = tautm x) (s : tm ) : subst_tm sigmatm s = subst_tm tautm s :=
match s return subst_tm sigmatm s = subst_tm tautm s with
| var_tm s => Eqtm s
| tAbs s0 => congr_tAbs ((ext_tm (up_tm_tm sigmatm) (up_tm_tm tautm) (upExt_tm_tm (_) (_) Eqtm)) s0)
| tApp s0 s1 => congr_tApp ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm sigmatm tautm Eqtm) s1)
| tPi s0 s1 => congr_tPi ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm (up_tm_tm sigmatm) (up_tm_tm tautm) (upExt_tm_tm (_) (_) Eqtm)) s1)
| tUniv s0 => congr_tUniv ((fun x => (eq_refl) x) s0)
| tEq s0 s1 s2 => congr_tEq ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm sigmatm tautm Eqtm) s1) ((ext_tm sigmatm tautm Eqtm) s2)
| tJ s0 s1 s2 s3 => congr_tJ ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm sigmatm tautm Eqtm) s1) ((ext_tm sigmatm tautm Eqtm) s2) ((ext_tm sigmatm tautm Eqtm) s3)
| tRefl => congr_tRefl
| tZero => congr_tZero
| tSuc s0 => congr_tSuc ((ext_tm sigmatm tautm Eqtm) s0)
| tInd s0 s1 s2 => congr_tInd ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm (up_tm_tm (up_tm_tm sigmatm)) (up_tm_tm (up_tm_tm tautm)) (upExt_tm_tm (_) (_) (upExt_tm_tm (_) (_) Eqtm))) s1) ((ext_tm sigmatm tautm Eqtm) s2)
| tNat => congr_tNat
| tSig s0 s1 => congr_tSig ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm (up_tm_tm sigmatm) (up_tm_tm tautm) (upExt_tm_tm (_) (_) Eqtm)) s1)
| tPack s0 s1 => congr_tPack ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm sigmatm tautm Eqtm) s1)
| tLet s0 s1 => congr_tLet ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm (up_tm_tm (up_tm_tm sigmatm)) (up_tm_tm (up_tm_tm tautm)) (upExt_tm_tm (_) (_) (upExt_tm_tm (_) (_) Eqtm))) s1)
end.
Definition up_ren_ren_tm_tm (xi : ( fin ) -> fin) (tau : ( fin ) -> fin) (theta : ( fin ) -> fin) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRen_tm_tm tau) (upRen_tm_tm xi)) x = (upRen_tm_tm theta) x :=
up_ren_ren xi tau theta Eq.
Fixpoint compRenRen_tm (xitm : ( fin ) -> fin) (zetatm : ( fin ) -> fin) (rhotm : ( fin ) -> fin) (Eqtm : forall x, ((funcomp) zetatm xitm) x = rhotm x) (s : tm ) : ren_tm zetatm (ren_tm xitm s) = ren_tm rhotm s :=
match s return ren_tm zetatm (ren_tm xitm s) = ren_tm rhotm s with
| var_tm s => (ap) (var_tm ) (Eqtm s)
| tAbs s0 => congr_tAbs ((compRenRen_tm (upRen_tm_tm xitm) (upRen_tm_tm zetatm) (upRen_tm_tm rhotm) (up_ren_ren (_) (_) (_) Eqtm)) s0)
| tApp s0 s1 => congr_tApp ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm xitm zetatm rhotm Eqtm) s1)
| tPi s0 s1 => congr_tPi ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm (upRen_tm_tm xitm) (upRen_tm_tm zetatm) (upRen_tm_tm rhotm) (up_ren_ren (_) (_) (_) Eqtm)) s1)
| tUniv s0 => congr_tUniv ((fun x => (eq_refl) x) s0)
| tEq s0 s1 s2 => congr_tEq ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm xitm zetatm rhotm Eqtm) s1) ((compRenRen_tm xitm zetatm rhotm Eqtm) s2)
| tJ s0 s1 s2 s3 => congr_tJ ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm xitm zetatm rhotm Eqtm) s1) ((compRenRen_tm xitm zetatm rhotm Eqtm) s2) ((compRenRen_tm xitm zetatm rhotm Eqtm) s3)
| tRefl => congr_tRefl
| tZero => congr_tZero
| tSuc s0 => congr_tSuc ((compRenRen_tm xitm zetatm rhotm Eqtm) s0)
| tInd s0 s1 s2 => congr_tInd ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm (upRen_tm_tm (upRen_tm_tm xitm)) (upRen_tm_tm (upRen_tm_tm zetatm)) (upRen_tm_tm (upRen_tm_tm rhotm)) (up_ren_ren (_) (_) (_) (up_ren_ren (_) (_) (_) Eqtm))) s1) ((compRenRen_tm xitm zetatm rhotm Eqtm) s2)
| tNat => congr_tNat
| tSig s0 s1 => congr_tSig ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm (upRen_tm_tm xitm) (upRen_tm_tm zetatm) (upRen_tm_tm rhotm) (up_ren_ren (_) (_) (_) Eqtm)) s1)
| tPack s0 s1 => congr_tPack ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm xitm zetatm rhotm Eqtm) s1)
| tLet s0 s1 => congr_tLet ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm (upRen_tm_tm (upRen_tm_tm xitm)) (upRen_tm_tm (upRen_tm_tm zetatm)) (upRen_tm_tm (upRen_tm_tm rhotm)) (up_ren_ren (_) (_) (_) (up_ren_ren (_) (_) (_) Eqtm))) s1)
end.
Definition up_ren_subst_tm_tm (xi : ( fin ) -> fin) (tau : ( fin ) -> tm ) (theta : ( fin ) -> tm ) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (up_tm_tm tau) (upRen_tm_tm xi)) x = (up_tm_tm theta) x :=
fun n => match n with
| S fin_n => (ap) (ren_tm (shift)) (Eq fin_n)
| 0 => eq_refl
end.
Fixpoint compRenSubst_tm (xitm : ( fin ) -> fin) (tautm : ( fin ) -> tm ) (thetatm : ( fin ) -> tm ) (Eqtm : forall x, ((funcomp) tautm xitm) x = thetatm x) (s : tm ) : subst_tm tautm (ren_tm xitm s) = subst_tm thetatm s :=
match s return subst_tm tautm (ren_tm xitm s) = subst_tm thetatm s with
| var_tm s => Eqtm s
| tAbs s0 => congr_tAbs ((compRenSubst_tm (upRen_tm_tm xitm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_ren_subst_tm_tm (_) (_) (_) Eqtm)) s0)
| tApp s0 s1 => congr_tApp ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm xitm tautm thetatm Eqtm) s1)
| tPi s0 s1 => congr_tPi ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm (upRen_tm_tm xitm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_ren_subst_tm_tm (_) (_) (_) Eqtm)) s1)
| tUniv s0 => congr_tUniv ((fun x => (eq_refl) x) s0)
| tEq s0 s1 s2 => congr_tEq ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm xitm tautm thetatm Eqtm) s1) ((compRenSubst_tm xitm tautm thetatm Eqtm) s2)
| tJ s0 s1 s2 s3 => congr_tJ ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm xitm tautm thetatm Eqtm) s1) ((compRenSubst_tm xitm tautm thetatm Eqtm) s2) ((compRenSubst_tm xitm tautm thetatm Eqtm) s3)
| tRefl => congr_tRefl
| tZero => congr_tZero
| tSuc s0 => congr_tSuc ((compRenSubst_tm xitm tautm thetatm Eqtm) s0)
| tInd s0 s1 s2 => congr_tInd ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm (upRen_tm_tm (upRen_tm_tm xitm)) (up_tm_tm (up_tm_tm tautm)) (up_tm_tm (up_tm_tm thetatm)) (up_ren_subst_tm_tm (_) (_) (_) (up_ren_subst_tm_tm (_) (_) (_) Eqtm))) s1) ((compRenSubst_tm xitm tautm thetatm Eqtm) s2)
| tNat => congr_tNat
| tSig s0 s1 => congr_tSig ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm (upRen_tm_tm xitm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_ren_subst_tm_tm (_) (_) (_) Eqtm)) s1)
| tPack s0 s1 => congr_tPack ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm xitm tautm thetatm Eqtm) s1)
| tLet s0 s1 => congr_tLet ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm (upRen_tm_tm (upRen_tm_tm xitm)) (up_tm_tm (up_tm_tm tautm)) (up_tm_tm (up_tm_tm thetatm)) (up_ren_subst_tm_tm (_) (_) (_) (up_ren_subst_tm_tm (_) (_) (_) Eqtm))) s1)
end.
Definition up_subst_ren_tm_tm (sigma : ( fin ) -> tm ) (zetatm : ( fin ) -> fin) (theta : ( fin ) -> tm ) (Eq : forall x, ((funcomp) (ren_tm zetatm) sigma) x = theta x) : forall x, ((funcomp) (ren_tm (upRen_tm_tm zetatm)) (up_tm_tm sigma)) x = (up_tm_tm theta) x :=
fun n => match n with
| S fin_n => (eq_trans) (compRenRen_tm (shift) (upRen_tm_tm zetatm) ((funcomp) (shift) zetatm) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compRenRen_tm zetatm (shift) ((funcomp) (shift) zetatm) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_tm (shift)) (Eq fin_n)))
| 0 => eq_refl
end.
Fixpoint compSubstRen_tm (sigmatm : ( fin ) -> tm ) (zetatm : ( fin ) -> fin) (thetatm : ( fin ) -> tm ) (Eqtm : forall x, ((funcomp) (ren_tm zetatm) sigmatm) x = thetatm x) (s : tm ) : ren_tm zetatm (subst_tm sigmatm s) = subst_tm thetatm s :=
match s return ren_tm zetatm (subst_tm sigmatm s) = subst_tm thetatm s with
| var_tm s => Eqtm s
| tAbs s0 => congr_tAbs ((compSubstRen_tm (up_tm_tm sigmatm) (upRen_tm_tm zetatm) (up_tm_tm thetatm) (up_subst_ren_tm_tm (_) (_) (_) Eqtm)) s0)
| tApp s0 s1 => congr_tApp ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s1)
| tPi s0 s1 => congr_tPi ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm (up_tm_tm sigmatm) (upRen_tm_tm zetatm) (up_tm_tm thetatm) (up_subst_ren_tm_tm (_) (_) (_) Eqtm)) s1)
| tUniv s0 => congr_tUniv ((fun x => (eq_refl) x) s0)
| tEq s0 s1 s2 => congr_tEq ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s1) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s2)
| tJ s0 s1 s2 s3 => congr_tJ ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s1) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s2) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s3)
| tRefl => congr_tRefl
| tZero => congr_tZero
| tSuc s0 => congr_tSuc ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0)
| tInd s0 s1 s2 => congr_tInd ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm (up_tm_tm (up_tm_tm sigmatm)) (upRen_tm_tm (upRen_tm_tm zetatm)) (up_tm_tm (up_tm_tm thetatm)) (up_subst_ren_tm_tm (_) (_) (_) (up_subst_ren_tm_tm (_) (_) (_) Eqtm))) s1) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s2)
| tNat => congr_tNat
| tSig s0 s1 => congr_tSig ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm (up_tm_tm sigmatm) (upRen_tm_tm zetatm) (up_tm_tm thetatm) (up_subst_ren_tm_tm (_) (_) (_) Eqtm)) s1)
| tPack s0 s1 => congr_tPack ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s1)
| tLet s0 s1 => congr_tLet ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm (up_tm_tm (up_tm_tm sigmatm)) (upRen_tm_tm (upRen_tm_tm zetatm)) (up_tm_tm (up_tm_tm thetatm)) (up_subst_ren_tm_tm (_) (_) (_) (up_subst_ren_tm_tm (_) (_) (_) Eqtm))) s1)
end.
Definition up_subst_subst_tm_tm (sigma : ( fin ) -> tm ) (tautm : ( fin ) -> tm ) (theta : ( fin ) -> tm ) (Eq : forall x, ((funcomp) (subst_tm tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (up_tm_tm tautm)) (up_tm_tm sigma)) x = (up_tm_tm theta) x :=
fun n => match n with
| S fin_n => (eq_trans) (compRenSubst_tm (shift) (up_tm_tm tautm) ((funcomp) (up_tm_tm tautm) (shift)) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compSubstRen_tm tautm (shift) ((funcomp) (ren_tm (shift)) tautm) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_tm (shift)) (Eq fin_n)))
| 0 => eq_refl
end.
Fixpoint compSubstSubst_tm (sigmatm : ( fin ) -> tm ) (tautm : ( fin ) -> tm ) (thetatm : ( fin ) -> tm ) (Eqtm : forall x, ((funcomp) (subst_tm tautm) sigmatm) x = thetatm x) (s : tm ) : subst_tm tautm (subst_tm sigmatm s) = subst_tm thetatm s :=
match s return subst_tm tautm (subst_tm sigmatm s) = subst_tm thetatm s with
| var_tm s => Eqtm s
| tAbs s0 => congr_tAbs ((compSubstSubst_tm (up_tm_tm sigmatm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_subst_subst_tm_tm (_) (_) (_) Eqtm)) s0)
| tApp s0 s1 => congr_tApp ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s1)
| tPi s0 s1 => congr_tPi ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm (up_tm_tm sigmatm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_subst_subst_tm_tm (_) (_) (_) Eqtm)) s1)
| tUniv s0 => congr_tUniv ((fun x => (eq_refl) x) s0)
| tEq s0 s1 s2 => congr_tEq ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s1) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s2)
| tJ s0 s1 s2 s3 => congr_tJ ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s1) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s2) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s3)
| tRefl => congr_tRefl
| tZero => congr_tZero
| tSuc s0 => congr_tSuc ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0)
| tInd s0 s1 s2 => congr_tInd ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm (up_tm_tm (up_tm_tm sigmatm)) (up_tm_tm (up_tm_tm tautm)) (up_tm_tm (up_tm_tm thetatm)) (up_subst_subst_tm_tm (_) (_) (_) (up_subst_subst_tm_tm (_) (_) (_) Eqtm))) s1) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s2)
| tNat => congr_tNat
| tSig s0 s1 => congr_tSig ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm (up_tm_tm sigmatm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_subst_subst_tm_tm (_) (_) (_) Eqtm)) s1)
| tPack s0 s1 => congr_tPack ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s1)
| tLet s0 s1 => congr_tLet ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm (up_tm_tm (up_tm_tm sigmatm)) (up_tm_tm (up_tm_tm tautm)) (up_tm_tm (up_tm_tm thetatm)) (up_subst_subst_tm_tm (_) (_) (_) (up_subst_subst_tm_tm (_) (_) (_) Eqtm))) s1)
end.
Definition rinstInst_up_tm_tm (xi : ( fin ) -> fin) (sigma : ( fin ) -> tm ) (Eq : forall x, ((funcomp) (var_tm ) xi) x = sigma x) : forall x, ((funcomp) (var_tm ) (upRen_tm_tm xi)) x = (up_tm_tm sigma) x :=
fun n => match n with
| S fin_n => (ap) (ren_tm (shift)) (Eq fin_n)
| 0 => eq_refl
end.
Fixpoint rinst_inst_tm (xitm : ( fin ) -> fin) (sigmatm : ( fin ) -> tm ) (Eqtm : forall x, ((funcomp) (var_tm ) xitm) x = sigmatm x) (s : tm ) : ren_tm xitm s = subst_tm sigmatm s :=
match s return ren_tm xitm s = subst_tm sigmatm s with
| var_tm s => Eqtm s
| tAbs s0 => congr_tAbs ((rinst_inst_tm (upRen_tm_tm xitm) (up_tm_tm sigmatm) (rinstInst_up_tm_tm (_) (_) Eqtm)) s0)
| tApp s0 s1 => congr_tApp ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm xitm sigmatm Eqtm) s1)
| tPi s0 s1 => congr_tPi ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm (upRen_tm_tm xitm) (up_tm_tm sigmatm) (rinstInst_up_tm_tm (_) (_) Eqtm)) s1)
| tUniv s0 => congr_tUniv ((fun x => (eq_refl) x) s0)
| tEq s0 s1 s2 => congr_tEq ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm xitm sigmatm Eqtm) s1) ((rinst_inst_tm xitm sigmatm Eqtm) s2)
| tJ s0 s1 s2 s3 => congr_tJ ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm xitm sigmatm Eqtm) s1) ((rinst_inst_tm xitm sigmatm Eqtm) s2) ((rinst_inst_tm xitm sigmatm Eqtm) s3)
| tRefl => congr_tRefl
| tZero => congr_tZero
| tSuc s0 => congr_tSuc ((rinst_inst_tm xitm sigmatm Eqtm) s0)
| tInd s0 s1 s2 => congr_tInd ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm (upRen_tm_tm (upRen_tm_tm xitm)) (up_tm_tm (up_tm_tm sigmatm)) (rinstInst_up_tm_tm (_) (_) (rinstInst_up_tm_tm (_) (_) Eqtm))) s1) ((rinst_inst_tm xitm sigmatm Eqtm) s2)
| tNat => congr_tNat
| tSig s0 s1 => congr_tSig ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm (upRen_tm_tm xitm) (up_tm_tm sigmatm) (rinstInst_up_tm_tm (_) (_) Eqtm)) s1)
| tPack s0 s1 => congr_tPack ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm xitm sigmatm Eqtm) s1)
| tLet s0 s1 => congr_tLet ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm (upRen_tm_tm (upRen_tm_tm xitm)) (up_tm_tm (up_tm_tm sigmatm)) (rinstInst_up_tm_tm (_) (_) (rinstInst_up_tm_tm (_) (_) Eqtm))) s1)
end.
Lemma rinstInst_tm (xitm : ( fin ) -> fin) : ren_tm xitm = subst_tm ((funcomp) (var_tm ) xitm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => rinst_inst_tm xitm (_) (fun n => eq_refl) x)). Qed.
Lemma instId_tm : subst_tm (var_tm ) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_tm (var_tm ) (fun n => eq_refl) ((id) x))). Qed.
Lemma rinstId_tm : @ren_tm (id) = id .
Proof. exact ((eq_trans) (rinstInst_tm ((id) (_))) instId_tm). Qed.
Lemma varL_tm (sigmatm : ( fin ) -> tm ) : (funcomp) (subst_tm sigmatm) (var_tm ) = sigmatm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.
Lemma varLRen_tm (xitm : ( fin ) -> fin) : (funcomp) (ren_tm xitm) (var_tm ) = (funcomp) (var_tm ) xitm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.
Lemma compComp_tm (sigmatm : ( fin ) -> tm ) (tautm : ( fin ) -> tm ) (s : tm ) : subst_tm tautm (subst_tm sigmatm s) = subst_tm ((funcomp) (subst_tm tautm) sigmatm) s .
Proof. exact (compSubstSubst_tm sigmatm tautm (_) (fun n => eq_refl) s). Qed.
Lemma compComp'_tm (sigmatm : ( fin ) -> tm ) (tautm : ( fin ) -> tm ) : (funcomp) (subst_tm tautm) (subst_tm sigmatm) = subst_tm ((funcomp) (subst_tm tautm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_tm sigmatm tautm n)). Qed.
Lemma compRen_tm (sigmatm : ( fin ) -> tm ) (zetatm : ( fin ) -> fin) (s : tm ) : ren_tm zetatm (subst_tm sigmatm s) = subst_tm ((funcomp) (ren_tm zetatm) sigmatm) s .
Proof. exact (compSubstRen_tm sigmatm zetatm (_) (fun n => eq_refl) s). Qed.
Lemma compRen'_tm (sigmatm : ( fin ) -> tm ) (zetatm : ( fin ) -> fin) : (funcomp) (ren_tm zetatm) (subst_tm sigmatm) = subst_tm ((funcomp) (ren_tm zetatm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compRen_tm sigmatm zetatm n)). Qed.
Lemma renComp_tm (xitm : ( fin ) -> fin) (tautm : ( fin ) -> tm ) (s : tm ) : subst_tm tautm (ren_tm xitm s) = subst_tm ((funcomp) tautm xitm) s .
Proof. exact (compRenSubst_tm xitm tautm (_) (fun n => eq_refl) s). Qed.
Lemma renComp'_tm (xitm : ( fin ) -> fin) (tautm : ( fin ) -> tm ) : (funcomp) (subst_tm tautm) (ren_tm xitm) = subst_tm ((funcomp) tautm xitm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renComp_tm xitm tautm n)). Qed.
Lemma renRen_tm (xitm : ( fin ) -> fin) (zetatm : ( fin ) -> fin) (s : tm ) : ren_tm zetatm (ren_tm xitm s) = ren_tm ((funcomp) zetatm xitm) s .
Proof. exact (compRenRen_tm xitm zetatm (_) (fun n => eq_refl) s). Qed.
Lemma renRen'_tm (xitm : ( fin ) -> fin) (zetatm : ( fin ) -> fin) : (funcomp) (ren_tm zetatm) (ren_tm xitm) = ren_tm ((funcomp) zetatm xitm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renRen_tm xitm zetatm n)). Qed.
End tm.
Global Instance Subst_tm : Subst1 (( fin ) -> tm ) (tm ) (tm ) := @subst_tm .
Global Instance Ren_tm : Ren1 (( fin ) -> fin) (tm ) (tm ) := @ren_tm .
Global Instance VarInstance_tm : Var (fin) (tm ) := @var_tm .
Notation "x '__tm'" := (var_tm x) (at level 5, format "x __tm") : subst_scope.
Notation "x '__tm'" := (@ids (_) (_) VarInstance_tm x) (at level 5, only printing, format "x __tm") : subst_scope.
Notation "'var'" := (var_tm) (only printing, at level 1) : subst_scope.
Class Up_tm X Y := up_tm : ( X ) -> Y.
Notation "↑__tm" := (up_tm) (only printing) : subst_scope.
Notation "↑__tm" := (up_tm_tm) (only printing) : subst_scope.
Global Instance Up_tm_tm : Up_tm (_) (_) := @up_tm_tm .
Notation "s [ sigmatm ]" := (subst_tm sigmatm s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmatm ]" := (subst_tm sigmatm) (at level 1, left associativity, only printing) : fscope.
Notation "s ⟨ xitm ⟩" := (ren_tm xitm s) (at level 7, left associativity, only printing) : subst_scope.
Notation "⟨ xitm ⟩" := (ren_tm xitm) (at level 1, left associativity, only printing) : fscope.
Ltac auto_unfold := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_tm, Ren_tm, VarInstance_tm.
Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_tm, Ren_tm, VarInstance_tm in *.
Ltac asimpl' := repeat first [progress rewrite ?instId_tm| progress rewrite ?compComp_tm| progress rewrite ?compComp'_tm| progress rewrite ?rinstId_tm| progress rewrite ?compRen_tm| progress rewrite ?compRen'_tm| progress rewrite ?renComp_tm| progress rewrite ?renComp'_tm| progress rewrite ?renRen_tm| progress rewrite ?renRen'_tm| progress rewrite ?varL_tm| progress rewrite ?varLRen_tm| progress (unfold up_ren, upRen_tm_tm, up_tm_tm)| progress (cbn [subst_tm ren_tm])| fsimpl].
Ltac asimpl := repeat try unfold_funcomp; auto_unfold in *; asimpl'; repeat try unfold_funcomp.
Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.
Tactic Notation "auto_case" := auto_case (asimpl; cbn; eauto).
Tactic Notation "asimpl" "in" "*" := auto_unfold in *; repeat first [progress rewrite ?instId_tm in *| progress rewrite ?compComp_tm in *| progress rewrite ?compComp'_tm in *| progress rewrite ?rinstId_tm in *| progress rewrite ?compRen_tm in *| progress rewrite ?compRen'_tm in *| progress rewrite ?renComp_tm in *| progress rewrite ?renComp'_tm in *| progress rewrite ?renRen_tm in *| progress rewrite ?renRen'_tm in *| progress rewrite ?varL_tm in *| progress rewrite ?varLRen_tm in *| progress (unfold up_ren, upRen_tm_tm, up_tm_tm in *)| progress (cbn [subst_tm ren_tm] in *)| fsimpl in *].
Ltac substify := auto_unfold; try repeat (erewrite rinstInst_tm).
Ltac renamify := auto_unfold; try repeat (erewrite <- rinstInst_tm).