-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathTermEquality.lp
3882 lines (3688 loc) · 215 KB
/
TermEquality.lp
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
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
require open ctt.ast;
require open ctt.DeBruijn;
require open ctt.Typing;
require open ctt.derived;
// Term equality, necessary to express commutation of different operations
constant symbol TEq : Term → Term → TYPE;
constant symbol TRefl (t : Term) : TEq t t;
constant symbol ITEq : ITerm → ITerm → TYPE;
constant symbol ITRefl (t : ITerm) : ITEq t t;
constant symbol FTEq : FTerm → FTerm → TYPE;
constant symbol FTRefl (t : FTerm) : FTEq t t;
// Elimination of term equality
symbol teq_inv [t1 t2 : Term] : TEq t1 t2 → TEq t2 t1;
symbol teq_trans [t1 t2 t3 : Term] : TEq t1 t2 → TEq t2 t3 → TEq t1 t3;
symbol Jt [Γ : Context] [s : Lev] [t1 t2 T : Term]
: TEq t1 t2 → der Γ t1 T s → der Γ t2 T s;
symbol JT [Γ : Context] [s : Lev] [t T1 T2 : Term]
: TEq T1 T2 → der Γ t T1 s → der Γ t T2 s;
symbol JtT [Γ : Context] [s : Lev] [t1 t2 T1 T2 : Term]
: TEq t1 t2 → TEq T1 T2 → der Γ t1 T1 s → der Γ t2 T2 s;
symbol Jcong [t1 t2 : Term] (f : Term → Term)
: TEq t1 t2 → TEq (f t1) (f t2);
symbol Jeq [Γ : Context] [s : Lev] [T T' t1 t1' t2 t2']
: TEq T T'
→ TEq t1 t1'
→ TEq t2 t2'
→ der_eq Γ t1 t2 T s
→ der_eq Γ t1' t2' T' s;
symbol dbcongT [i j : DBId] (f : DBId → Term) : DBEq i j → TEq (f i) (f j);
symbol IcongT [i j : ITerm] (f : ITerm → Term) : ITEq i j → TEq (f i) (f j);
symbol FcongT [i j : FTerm] (f : FTerm → Term) : FTEq i j → TEq (f i) (f j);
rule teq_inv (TRefl $t) ↪ TRefl $t
with teq_trans (TRefl $t) (TRefl _) ↪ TRefl $t
with JtT (TRefl _) (TRefl _) $d ↪ $d
with @Jt _ _ _ _ $T $eqt $d ↪ JtT $eqt (TRefl $T) $d
with @JT _ _ $t _ _ $eqT $d ↪ JtT (TRefl $t) $eqT $d
with @Jcong $t _ $f (TRefl _) ↪ TRefl ($f $t)
with Jeq (TRefl _) (TRefl _) (TRefl _) $d ↪ $d
with dbcongT $f (DBRefl $i) ↪ TRefl ($f $i)
with IcongT $f (ITRefl $i) ↪ TRefl ($f $i)
with FcongT $f (FTRefl $i) ↪ TRefl ($f $i);
// Congruence for term equality
symbol Jpi [A1 A2 B1 B2 : Term] :
TEq A1 A2 → TEq B1 B2 → TEq (tpi A1 B1) (tpi A2 B2);
symbol Jabs [A1 A2 t1 t2 : Term] :
TEq A1 A2 → TEq t1 t2 → TEq (tabs A1 t1) (tabs A2 t2);
symbol Japp [f1 f2 a1 a2 : Term] :
TEq f1 f2 → TEq a1 a2 → TEq (tapp f1 a1) (tapp f2 a2);
symbol Jrec [P1 P2 z1 z2 H1 H2 n1 n2] :
TEq P1 P2 → TEq z1 z2 → TEq H1 H2 → TEq n1 n2 → TEq (trec P1 z1 H1 n1) (trec P2 z2 H2 n2);
symbol Jsig [A1 A2 B1 B2] :
TEq A1 A2 → TEq B1 B2 → TEq (tsig A1 B1) (tsig A2 B2);
symbol Jpair [a1 a2 b1 b2 : Term] :
TEq a1 a2 → TEq b1 b2 → TEq (tpair a1 b1) (tpair a2 b2);
symbol Jsum [A1 A2 B1 B2 : Term] :
TEq A1 A2 → TEq B1 B2 → TEq (tsum A1 B1) (tsum A2 B2);
symbol Jcase [P1 P2 A1 A2 B1 B2 Ha1 Ha2 Hb1 Hb2 t1 t2] :
TEq P1 P2 → TEq A1 A2 → TEq B1 B2 → TEq Ha1 Ha2 → TEq Hb1 Hb2 → TEq t1 t2 →
TEq (tcase P1 A1 B1 Ha1 Hb1 t1) (tcase P2 A2 B2 Ha2 Hb2 t2);
symbol Jpath [A1 A2 x1 x2 y1 y2] :
TEq A1 A2 → TEq x1 x2 → TEq y1 y2 → TEq (tpath A1 x1 y1) (tpath A2 x2 y2);
symbol JappP [u1 u2 v1 v2] :
TEq u1 u2 → ITEq v1 v2 → TEq (tappP u1 v1) (tappP u2 v2);
symbol Jsys [f1 f2 g1 g2 u1 u2 v1 v2] :
FTEq f1 f2 → FTEq g1 g2 → TEq u1 u2 → TEq v1 v2 → TEq (tsys f1 g1 u1 v1) (tsys f2 g2 u2 v2);
symbol Jtransp [A1 A2 f1 f2 u1 u2] :
TEq A1 A2 → FTEq f1 f2 → TEq u1 u2 → TEq (ttransp A1 f1 u1) (ttransp A2 f2 u2);
symbol Jhcomp [A1 A2 f1 f2 u1 u2 v1 v2] :
TEq A1 A2 → FTEq f1 f2 → TEq u1 u2 → TEq v1 v2 → TEq (thcomp A1 f1 u1 v1) (thcomp A2 f2 u2 v2);
symbol Jselect [eq1 eq2 gt1 gt2 lt1 lt2 : Term] (i j : DBId) :
TEq eq1 eq2 → TEq gt1 gt2 → TEq lt1 lt2 →
TEq (dbselect i j eq1 gt1 lt1) (dbselect i j eq2 gt2 lt2);
rule Jpi (TRefl _) (TRefl _) ↪ TRefl _
with Jabs (TRefl _) (TRefl _) ↪ TRefl _
with Japp (TRefl _) (TRefl _) ↪ TRefl _
with Jrec (TRefl _) (TRefl _) (TRefl _) (TRefl _) ↪ TRefl _
with Jsig (TRefl _) (TRefl _) ↪ TRefl _
with Jpair (TRefl _) (TRefl _) ↪ TRefl _
with Jsum (TRefl _) (TRefl _) ↪ TRefl _
with Jcase (TRefl _) (TRefl _) (TRefl _) (TRefl _) (TRefl _) (TRefl _) ↪ TRefl _
with Jpath (TRefl _) (TRefl _) (TRefl _) ↪ TRefl _
with JappP (TRefl _) (ITRefl _) ↪ TRefl _
with Jsys (FTRefl _) (FTRefl _) (TRefl _) (TRefl _) ↪ TRefl _
with Jtransp (TRefl _) (FTRefl _) (TRefl _) ↪ TRefl _
with Jhcomp (TRefl _) (FTRefl _) (TRefl _) (TRefl _) ↪ TRefl _
with Jselect $i $j (TRefl $eq) (TRefl $gt) (TRefl $lt) ↪ TRefl (dbselect $i $j $eq $gt $lt);
// Elimination of interval term equality
symbol iteq_inv [t1 t2 : ITerm] : ITEq t1 t2 → ITEq t2 t1;
symbol iteq_trans [t1 t2 t3 : ITerm] : ITEq t1 t2 → ITEq t2 t3 → ITEq t1 t3;
symbol IJ [Γ : Context] [t1 t2 : ITerm]
: ITEq t1 t2 → der_I Γ t1 → der_I Γ t2;
symbol IJcong [t1 t2 : ITerm] (f : ITerm → ITerm)
: ITEq t1 t2 → ITEq (f t1) (f t2);
symbol IJeq [Γ : Context] [t1 t1' t2 t2']
: ITEq t1 t1'
→ ITEq t2 t2'
→ der_eq_I Γ t1 t2
→ der_eq_I Γ t1' t2';
symbol dbcongI [i j : DBId] (f : DBId → ITerm) : DBEq i j → ITEq (f i) (f j);
rule iteq_inv (ITRefl $t) ↪ ITRefl $t
with iteq_trans (ITRefl $t) (ITRefl _) ↪ ITRefl $t
with IJ (ITRefl _) $d ↪ $d
with @IJcong $t _ $f (ITRefl _) ↪ ITRefl ($f $t)
with IJeq (ITRefl _) (ITRefl _) $d ↪ $d
with dbcongI $f (DBRefl $i) ↪ ITRefl ($f $i);
// Congruence for interval term equality
symbol IJmin [i1 i2 j1 j2] :
ITEq i1 i2 → ITEq j1 j2 → ITEq (itmin i1 j1) (itmin i2 j2);
symbol IJmax [i1 i2 j1 j2] :
ITEq i1 i2 → ITEq j1 j2 → ITEq (itmax i1 j1) (itmax i2 j2);
symbol IJselect [eq1 eq2 gt1 gt2 lt1 lt2 : ITerm] (i j : DBId) :
ITEq eq1 eq2 → ITEq gt1 gt2 → ITEq lt1 lt2 →
ITEq (dbselectI i j eq1 gt1 lt1) (dbselectI i j eq2 gt2 lt2);
rule IJmin (ITRefl _) (ITRefl _) ↪ ITRefl _
with IJmax (ITRefl _) (ITRefl _) ↪ ITRefl _
with IJselect _ _ (ITRefl _) (ITRefl _) (ITRefl _) ↪ ITRefl _;
// Elimination of face term equality
symbol fteq_inv [t1 t2 : FTerm] : FTEq t1 t2 → FTEq t2 t1;
symbol fteq_trans [t1 t2 t3 : FTerm] : FTEq t1 t2 → FTEq t2 t3 → FTEq t1 t3;
symbol FJ [Γ : Context] [t1 t2 : FTerm]
: FTEq t1 t2 → der_F Γ t1 → der_F Γ t2;
symbol FJcong [t1 t2 : FTerm] (f : FTerm → FTerm)
: FTEq t1 t2 → FTEq (f t1) (f t2);
symbol FJeq [Γ : Context] [t1 t1' t2 t2']
: FTEq t1 t1'
→ FTEq t2 t2'
→ der_eq_F Γ t1 t2
→ der_eq_F Γ t1' t2';
symbol FJisOne [Γ : Context] [t1 t2 : FTerm] :
FTEq t1 t2 → der_isOne Γ t1 → der_isOne Γ t2;
symbol dbcongF [i j : DBId] (f : DBId → FTerm) : DBEq i j → FTEq (f i) (f j);
symbol IcongF [i j : ITerm] (f : ITerm → FTerm) : ITEq i j → FTEq (f i) (f j);
rule fteq_inv (FTRefl $t) ↪ FTRefl $t
with fteq_trans (FTRefl $t) (FTRefl _) ↪ FTRefl $t
with FJ (FTRefl _) $d ↪ $d
with @FJcong $t _ $f (FTRefl _) ↪ FTRefl ($f $t)
with FJeq (FTRefl _) (FTRefl _) $d ↪ $d
with FJisOne (FTRefl _) $d ↪ $d
with dbcongF $f (DBRefl $i) ↪ FTRefl ($f $i)
with IcongF $f (ITRefl $i) ↪ FTRefl ($f $i);
// Congruence for face term equality
symbol FJmin [i1 i2 j1 j2] :
FTEq i1 i2 → FTEq j1 j2 → FTEq (ftmin i1 j1) (ftmin i2 j2);
symbol FJmax [i1 i2 j1 j2] :
FTEq i1 i2 → FTEq j1 j2 → FTEq (ftmax i1 j1) (ftmax i2 j2);
symbol FJselect [eq1 eq2 gt1 gt2 lt1 lt2 : FTerm] (i j : DBId) :
FTEq eq1 eq2 → FTEq gt1 gt2 → FTEq lt1 lt2 →
FTEq (dbselectF i j eq1 gt1 lt1) (dbselectF i j eq2 gt2 lt2);
rule FJmin (FTRefl _) (FTRefl _) ↪ FTRefl _
with FJmax (FTRefl _) (FTRefl _) ↪ FTRefl _
with FJselect _ _ (FTRefl _) (FTRefl _) (FTRefl _) ↪ FTRefl _;
// Auxiliary lemmas
// Arbitrary sequences of shift applied to terms we're substituting
// One regular substitution
constant symbol ShiftSequence : DBId → TYPE;
constant symbol SS0 : ShiftSequence db0;
constant symbol SSP [i : DBId] : ShiftSequence i → ShiftSequence (dbsucc i);
constant symbol SSI [i : DBId] : ShiftSequence i → ShiftSequence i;
symbol shift_seq [i : DBId] : ShiftSequence i → Term → Term;
rule shift_seq SS0 $t ↪ $t
with shift_seq (SSP $ss) $t ↪ Shift (shift_seq $ss $t)
with shift_seq (SSI $ss) $t ↪ IShift (shift_seq $ss $t);
// A second (later) substitution
constant symbol DoubleSequence : DBId → DBId → TYPE;
constant symbol DS0 [i : DBId] : ShiftSequence i → DoubleSequence i db0;
constant symbol DSP [i j : DBId] : DoubleSequence i j → DoubleSequence (dbsucc i) (dbsucc j);
constant symbol DSI [i j : DBId] : DoubleSequence i j → DoubleSequence i j;
symbol shift_dseq [i j : DBId] : DoubleSequence i j → Term → Term;
rule shift_dseq (DS0 $ss) $t ↪ (shift_seq $ss $t)
with shift_dseq (DSP $ds) $t ↪ Shift (shift_dseq $ds $t)
with shift_dseq (DSI $ds) $t ↪ IShift (shift_dseq $ds $t);
symbol shift_dseq2 [i j : DBId] : DoubleSequence i j → Term → Term;
rule shift_dseq2 (DS0 _) $t ↪ $t
with shift_dseq2 (DSP $ds) $t ↪ Shift (shift_dseq2 $ds $t)
with shift_dseq2 (DSI $ds) $t ↪ IShift (shift_dseq2 $ds $t);
// One interval substitution
constant symbol IShiftSequence : DBId → TYPE;
constant symbol IS0 : IShiftSequence db0;
constant symbol ISP [i : DBId] : IShiftSequence i → IShiftSequence i;
constant symbol ISI [i : DBId] : IShiftSequence i → IShiftSequence (dbsucc i);
symbol Ishift_seq [i : DBId] : IShiftSequence i → ITerm → ITerm;
rule Ishift_seq IS0 $t ↪ $t
with Ishift_seq (ISP $is) $t ↪ Ishift_seq $is $t
with Ishift_seq (ISI $is) $t ↪ IShiftI (Ishift_seq $is $t);
// A second (later) substitution
constant symbol IDoubleSequence : DBId → DBId → TYPE;
constant symbol IDS0 [i : DBId] : IShiftSequence i → IDoubleSequence i db0;
constant symbol IDSP [i j : DBId] : IDoubleSequence i j → IDoubleSequence i j;
constant symbol IDSI [i j : DBId] : IDoubleSequence i j → IDoubleSequence (dbsucc i) (dbsucc j);
symbol Ishift_dseq [i j : DBId] : IDoubleSequence i j → ITerm → ITerm;
rule Ishift_dseq (IDS0 $is) $t ↪ (Ishift_seq $is $t)
with Ishift_dseq (IDSP $ds) $t ↪ Ishift_dseq $ds $t
with Ishift_dseq (IDSI $ds) $t ↪ IShiftI (Ishift_dseq $ds $t);
symbol Ishift_dseq2 [i j : DBId] : IDoubleSequence i j → ITerm → ITerm;
rule Ishift_dseq2 (IDS0 _) $t ↪ $t
with Ishift_dseq2 (IDSP $ds) $t ↪ Ishift_dseq2 $ds $t
with Ishift_dseq2 (IDSI $ds) $t ↪ IShiftI (Ishift_dseq2 $ds $t);
// Both interval and regular substitutions
constant symbol MixedSequence : DBId → DBId → TYPE;
constant symbol MS0I [i : DBId] : ShiftSequence i → MixedSequence i db0;
constant symbol MS0R [i : DBId] : IShiftSequence i → MixedSequence db0 i;
constant symbol MSP [i j : DBId] : MixedSequence i j → MixedSequence (dbsucc i) j;
constant symbol MSI [i j : DBId] : MixedSequence i j → MixedSequence i (dbsucc j);
symbol shift_mseq [i j : DBId] : MixedSequence i j → Term → Term;
rule shift_mseq (MS0I $ss) $t ↪ shift_seq $ss $t
with shift_mseq (MS0R _) $t ↪ $t
with shift_mseq (MSP $ms) $t ↪ Shift (shift_mseq $ms $t)
with shift_mseq (MSI $ms) $t ↪ IShift (shift_mseq $ms $t);
symbol Ishift_mseq [i j : DBId] : MixedSequence i j → ITerm → ITerm;
rule Ishift_mseq (MS0I _) $t ↪ $t
with Ishift_mseq (MS0R $is) $t ↪ Ishift_seq $is $t
with Ishift_mseq (MSP $ds) $t ↪ Ishift_mseq $ds $t
with Ishift_mseq (MSI $ds) $t ↪ IShiftI (Ishift_mseq $ds $t);
// regular then interval substitution
constant symbol IMixedSequence : DBId → DBId → TYPE;
constant symbol IM0 [i : DBId] : ShiftSequence i → IMixedSequence i db0;
constant symbol IMP [i j : DBId] : IMixedSequence i j → IMixedSequence (dbsucc i) j;
constant symbol IMI [i j : DBId] : IMixedSequence i j → IMixedSequence i (dbsucc j);
symbol shift_imseq [i j : DBId] : IMixedSequence i j → Term → Term;
rule shift_imseq (IM0 $ss) $t ↪ shift_seq $ss $t
with shift_imseq (IMP $ms) $t ↪ Shift (shift_imseq $ms $t)
with shift_imseq (IMI [_] [$j] $ms) $t ↪ Ishift $j (shift_imseq $ms $t);
symbol Ishift_imseq [i j : DBId] : IMixedSequence i j → ITerm → ITerm;
rule Ishift_imseq (IM0 _) $t ↪ $t
with Ishift_imseq (IMP $ds) $t ↪ Ishift_imseq $ds $t
with Ishift_imseq (IMI [_] [$j] $ds) $t ↪ IshiftI $j (Ishift_imseq $ds $t);
// Both interval and regular substitutions, careful substituting
constant symbol NMixedSequence : DBId → DBId → TYPE;
constant symbol NM0 : NMixedSequence db0 db0;
constant symbol NMP [i j : DBId] : NMixedSequence i j → NMixedSequence (dbsucc i) j;
constant symbol NMI [i j : DBId] : NMixedSequence i j → NMixedSequence i (dbsucc j);
symbol shift_nmseq [i j : DBId] : NMixedSequence i j → Term → Term;
rule shift_nmseq NM0 $t ↪ $t
with shift_nmseq (NMP [$i] $ms) $t ↪ shift $i (shift_nmseq $ms $t)
with shift_nmseq (@NMI _ $j $ms) $t ↪ Ishift $j (shift_nmseq $ms $t);
symbol Ishift_nmseq [i j : DBId] : NMixedSequence i j → ITerm → ITerm;
rule Ishift_nmseq NM0 $t ↪ $t
with Ishift_nmseq (NMP $ds) $t ↪ Ishift_nmseq $ds $t
with Ishift_nmseq (@NMI _ $j $ds) $t ↪ IshiftI $j (Ishift_nmseq $ds $t);
constant symbol DMixedSequence : DBId → DBId → DBId → DBId → TYPE;
constant symbol DM0I [i j : DBId] : NMixedSequence i j → DMixedSequence i j db0 db0;
constant symbol DM0R [i j : DBId] : NMixedSequence i j → DMixedSequence db0 db0 i j;
constant symbol DMP [i j i' j' : DBId] : DMixedSequence i j i' j' → DMixedSequence (dbsucc i) j (dbsucc i') j';
constant symbol DMI [i j i' j' : DBId] : DMixedSequence i j i' j' → DMixedSequence i (dbsucc j) i' (dbsucc j');
symbol shift_dmseq [i j i' j' : DBId] : DMixedSequence i j i' j' → Term → Term;
rule shift_dmseq (DM0I $ss) $t ↪ shift_nmseq $ss $t
with shift_dmseq (DM0R _) $t ↪ $t
with shift_dmseq (DMP [$i] $ms) $t ↪ shift $i (shift_dmseq $ms $t)
with shift_dmseq (DMI [_] [$j] $ms) $t ↪ Ishift $j (shift_dmseq $ms $t);
symbol Ishift_dmseq [i j i' j' : DBId] : DMixedSequence i j i' j' → ITerm → ITerm;
rule Ishift_dmseq (DM0I _) $t ↪ $t
with Ishift_dmseq (DM0R $is) $t ↪ Ishift_nmseq $is $t
with Ishift_dmseq (DMP $ds) $t ↪ Ishift_dmseq $ds $t
with Ishift_dmseq (@DMI _ _ _ $j $ds) $t ↪ IshiftI $j (Ishift_dmseq $ds $t);
// shift_lt
symbol aux_dbshift_le (i j : DBId) : DBLe j (dbshift i j);
rule aux_dbshift_le db0 $j ↪ DBLe_succ (DBLe_refl $j)
with aux_dbshift_le (dbsucc _) db0 ↪ DBLe_refl db0
with aux_dbshift_le (dbsucc $i) (dbsucc $j) ↪ dble_n_S (aux_dbshift_le $i $j);
symbol aux_dbshift_le_refl (i j : DBId) : DBLe j i → DBEq j (dbshift (dbsucc i) j);
rule aux_dbshift_le_refl _ db0 _ ↪ DBRefl _
with aux_dbshift_le_refl (dbsucc $i) (dbsucc $j) $h ↪ dbcong dbsucc (aux_dbshift_le_refl $i $j (dble_S_n $h));
symbol aux_dbshift_lt_refl (i j : DBId) : DBLe (dbsucc j) i → DBEq j (dbshift i j);
rule aux_dbshift_lt_refl (dbsucc _) db0 _ ↪ DBRefl _
with aux_dbshift_lt_refl (dbsucc $i) (dbsucc $j) $h ↪ dbcong dbsucc (aux_dbshift_lt_refl $i $j (dble_S_n $h));
symbol aux_dbshift_le_succ (i j : DBId) : DBLe i j → DBEq (dbsucc j) (dbshift i j);
rule aux_dbshift_le_succ db0 _ _ ↪ DBRefl _
with aux_dbshift_le_succ (dbsucc $i) (dbsucc $j) $h ↪ dbcong dbsucc (aux_dbshift_le_succ $i $j (dble_S_n $h));
symbol aux_dbshift_dbprev (i j k : DBId) : DBLe (dbsucc k) j →
DBEq (dbprev (dbshift (dbsucc i) j)) (dbshift i (dbprev j));
rule aux_dbshift_dbprev db0 (dbsucc _) _ _ ↪ DBRefl _
with aux_dbshift_dbprev (dbsucc _) (dbsucc _) _ _ ↪ DBRefl _;
// dbselect*_spec_eq
symbol aux_dbselect_spec_eq (i j : DBId) (eqT gtT ltT : Term) :
DBEq i j → TEq (dbselect i j eqT gtT ltT) eqT;
rule aux_dbselect_spec_eq db0 db0 $eqT _ _ _ ↪ TRefl $eqT
with aux_dbselect_spec_eq (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT $h ↪
aux_dbselect_spec_eq $i $j $eqT $gtT $ltT (dbeq_S_n $h);
symbol aux_dbselectI_spec_eq (i j : DBId) (eqT gtT ltT : ITerm) :
DBEq i j → ITEq (dbselectI i j eqT gtT ltT) eqT;
rule aux_dbselectI_spec_eq db0 db0 $eqT _ _ _ ↪ ITRefl $eqT
with aux_dbselectI_spec_eq (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT $h ↪
aux_dbselectI_spec_eq $i $j $eqT $gtT $ltT (dbeq_S_n $h);
symbol aux_dbselectF_spec_eq (i j : DBId) (eqT gtT ltT : FTerm) :
DBEq i j → FTEq (dbselectF i j eqT gtT ltT) eqT;
rule aux_dbselectF_spec_eq db0 db0 $eqT _ _ _ ↪ FTRefl $eqT
with aux_dbselectF_spec_eq (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT $h ↪
aux_dbselectF_spec_eq $i $j $eqT $gtT $ltT (dbeq_S_n $h);
// dbselect*_spec_lt
symbol aux_dbselect_spec_lt (i j : DBId) (eqT gtT ltT : Term) :
DBLe (dbsucc i) j → TEq (dbselect i j eqT gtT ltT) ltT;
rule aux_dbselect_spec_lt db0 (dbsucc _) _ _ $ltT _ ↪ TRefl $ltT
with aux_dbselect_spec_lt (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT $h ↪
aux_dbselect_spec_lt $i $j $eqT $gtT $ltT (dble_S_n $h);
symbol aux_dbselectI_spec_lt (i j : DBId) (eqT gtT ltT : ITerm) :
DBLe (dbsucc i) j → ITEq (dbselectI i j eqT gtT ltT) ltT;
rule aux_dbselectI_spec_lt db0 (dbsucc _) _ _ $ltT _ ↪ ITRefl $ltT
with aux_dbselectI_spec_lt (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT $h ↪
aux_dbselectI_spec_lt $i $j $eqT $gtT $ltT (dble_S_n $h);
symbol aux_dbselectF_spec_lt (i j : DBId) (eqT gtT ltT : FTerm) :
DBLe (dbsucc i) j → FTEq (dbselectF i j eqT gtT ltT) ltT;
rule aux_dbselectF_spec_lt db0 (dbsucc _) _ _ $ltT _ ↪ FTRefl $ltT
with aux_dbselectF_spec_lt (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT $h ↪
aux_dbselectF_spec_lt $i $j $eqT $gtT $ltT (dble_S_n $h);
// dbselect*_spec_gt
symbol aux_dbselect_spec_gt (i j : DBId) (eqT gtT ltT : Term) :
DBLe (dbsucc j) i → TEq (dbselect i j eqT gtT ltT) gtT;
rule aux_dbselect_spec_gt (dbsucc _) db0 _ $gtT _ _ ↪ TRefl $gtT
with aux_dbselect_spec_gt (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT $h ↪
aux_dbselect_spec_gt $i $j $eqT $gtT $ltT (dble_S_n $h);
symbol aux_dbselectI_spec_gt (i j : DBId) (eqT gtT ltT : ITerm) :
DBLe (dbsucc j) i → ITEq (dbselectI i j eqT gtT ltT) gtT;
rule aux_dbselectI_spec_gt (dbsucc _) db0 _ $gtT _ _ ↪ ITRefl $gtT
with aux_dbselectI_spec_gt (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT $h ↪
aux_dbselectI_spec_gt $i $j $eqT $gtT $ltT (dble_S_n $h);
symbol aux_dbselectF_spec_gt (i j : DBId) (eqT gtT ltT : FTerm) :
DBLe (dbsucc j) i → FTEq (dbselectF i j eqT gtT ltT) gtT;
rule aux_dbselectF_spec_gt (dbsucc _) db0 _ $gtT _ _ ↪ FTRefl $gtT
with aux_dbselectF_spec_gt (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT $h ↪
aux_dbselectF_spec_gt $i $j $eqT $gtT $ltT (dble_S_n $h);
// dbselect*_spec_match
symbol aux_dbselect_spec_match (i j : DBId) (eq gt lt t : Term) :
(DBEq i j → TEq (dbselect i j eq gt lt) t) →
(DBLe (dbsucc j) i → TEq (dbselect i j eq gt lt) t) →
(DBLe (dbsucc i) j → TEq (dbselect i j eq gt lt) t) →
TEq (dbselect i j eq gt lt) t;
rule aux_dbselect_spec_match db0 db0 _ _ _ _ $e _ _ ↪ $e (DBRefl db0)
with aux_dbselect_spec_match (dbsucc $i) db0 _ _ _ _ _ $e _ ↪ $e (dble_n_S (dble_0_n $i))
with aux_dbselect_spec_match db0 (dbsucc $j) _ _ _ _ _ _ $e ↪ $e (dble_n_S (dble_0_n $j))
with aux_dbselect_spec_match (dbsucc $i) (dbsucc $j) $eq $gt $lt $t $e $g $l ↪
aux_dbselect_spec_match $i $j $eq $gt $lt $t (λ p, $e (dbcong dbsucc p)) (λ p, $g (dble_n_S p)) (λ p, $l (dble_n_S p));
symbol aux_dbselectI_spec_match (i j : DBId) (eq gt lt t : ITerm) :
(DBEq i j → ITEq (dbselectI i j eq gt lt) t) →
(DBLe (dbsucc j) i → ITEq (dbselectI i j eq gt lt) t) →
(DBLe (dbsucc i) j → ITEq (dbselectI i j eq gt lt) t) →
ITEq (dbselectI i j eq gt lt) t;
rule aux_dbselectI_spec_match db0 db0 _ _ _ _ $e _ _ ↪ $e (DBRefl db0)
with aux_dbselectI_spec_match (dbsucc $i) db0 _ _ _ _ _ $e _ ↪ $e (dble_n_S (dble_0_n $i))
with aux_dbselectI_spec_match db0 (dbsucc $j) _ _ _ _ _ _ $e ↪ $e (dble_n_S (dble_0_n $j))
with aux_dbselectI_spec_match (dbsucc $i) (dbsucc $j) $eq $gt $lt $t $e $g $l ↪
aux_dbselectI_spec_match $i $j $eq $gt $lt $t (λ p, $e (dbcong dbsucc p)) (λ p, $g (dble_n_S p)) (λ p, $l (dble_n_S p));
symbol aux_dbselectF_spec_match (i j : DBId) (eq gt lt t : FTerm) :
(DBEq i j → FTEq (dbselectF i j eq gt lt) t) →
(DBLe (dbsucc j) i → FTEq (dbselectF i j eq gt lt) t) →
(DBLe (dbsucc i) j → FTEq (dbselectF i j eq gt lt) t) →
FTEq (dbselectF i j eq gt lt) t;
rule aux_dbselectF_spec_match db0 db0 _ _ _ _ $e _ _ ↪ $e (DBRefl db0)
with aux_dbselectF_spec_match (dbsucc $i) db0 _ _ _ _ _ $e _ ↪ $e (dble_n_S (dble_0_n $i))
with aux_dbselectF_spec_match db0 (dbsucc $j) _ _ _ _ _ _ $e ↪ $e (dble_n_S (dble_0_n $j))
with aux_dbselectF_spec_match (dbsucc $i) (dbsucc $j) $eq $gt $lt $t $e $g $l ↪
aux_dbselectF_spec_match $i $j $eq $gt $lt $t (λ p, $e (dbcong dbsucc p)) (λ p, $g (dble_n_S p)) (λ p, $l (dble_n_S p));
// dbselect*_cong
symbol aux_dbselect_cong_match (i j : DBId) [eq gt lt eq' gt' lt' : Term] :
(DBEq i j → TEq eq eq') →
(DBLe (dbsucc j) i → TEq gt gt') →
(DBLe (dbsucc i) j → TEq lt lt') →
TEq (dbselect i j eq gt lt) (dbselect i j eq' gt' lt');
rule aux_dbselect_cong_match db0 db0 $e _ _ ↪ $e (DBRefl db0)
with aux_dbselect_cong_match (dbsucc $i) db0 _ $e _ ↪ $e (dble_n_S (dble_0_n $i))
with aux_dbselect_cong_match db0 (dbsucc $j) _ _ $e ↪ $e (dble_n_S (dble_0_n $j))
with aux_dbselect_cong_match (dbsucc $i) (dbsucc $j) $e $g $l ↪
aux_dbselect_cong_match $i $j (λ p, $e (dbcong dbsucc p)) (λ p, $g (dble_n_S p)) (λ p, $l (dble_n_S p));
symbol aux_dbselectI_cong_match (i j : DBId) [eq gt lt eq' gt' lt' : ITerm] :
(DBEq i j → ITEq eq eq') →
(DBLe (dbsucc j) i → ITEq gt gt') →
(DBLe (dbsucc i) j → ITEq lt lt') →
ITEq (dbselectI i j eq gt lt) (dbselectI i j eq' gt' lt');
rule aux_dbselectI_cong_match db0 db0 $e _ _ ↪ $e (DBRefl db0)
with aux_dbselectI_cong_match (dbsucc $i) db0 _ $e _ ↪ $e (dble_n_S (dble_0_n $i))
with aux_dbselectI_cong_match db0 (dbsucc $j) _ _ $e ↪ $e (dble_n_S (dble_0_n $j))
with aux_dbselectI_cong_match (dbsucc $i) (dbsucc $j) $e $g $l ↪
aux_dbselectI_cong_match $i $j (λ p, $e (dbcong dbsucc p)) (λ p, $g (dble_n_S p)) (λ p, $l (dble_n_S p));
symbol aux_dbselectF_cong_match (i j : DBId) [eq gt lt eq' gt' lt' : FTerm] :
(DBEq i j → FTEq eq eq') →
(DBLe (dbsucc j) i → FTEq gt gt') →
(DBLe (dbsucc i) j → FTEq lt lt') →
FTEq (dbselectF i j eq gt lt) (dbselectF i j eq' gt' lt');
rule aux_dbselectF_cong_match db0 db0 $e _ _ ↪ $e (DBRefl db0)
with aux_dbselectF_cong_match (dbsucc $i) db0 _ $e _ ↪ $e (dble_n_S (dble_0_n $i))
with aux_dbselectF_cong_match db0 (dbsucc $j) _ _ $e ↪ $e (dble_n_S (dble_0_n $j))
with aux_dbselectF_cong_match (dbsucc $i) (dbsucc $j) $e $g $l ↪
aux_dbselectF_cong_match $i $j (λ p, $e (dbcong dbsucc p)) (λ p, $g (dble_n_S p)) (λ p, $l (dble_n_S p));
// teq_shift_shift
symbol aux_teq_shift_shift (i j : DBId) (u : Term) :
DBLe i j → TEq (shift i (shift j u)) (shift (dbsucc j) (shift i u));
symbol aux_teq_shift_shift_var (i j n : DBId) :
DBLe i j → DBEq (dbshift i (dbshift j n)) (dbshift (dbsucc j) (dbshift i n));
rule aux_teq_shift_shift_var db0 $j $n _ ↪ DBRefl (dbsucc (dbshift $j $n))
with aux_teq_shift_shift_var (dbsucc _) (dbsucc _) db0 _ ↪ DBRefl db0
with aux_teq_shift_shift_var (dbsucc $i) (dbsucc $j) (dbsucc $n) $h ↪
dbcong dbsucc (aux_teq_shift_shift_var $i $j $n (dble_S_n $h))
with aux_teq_shift_shift $i $j (tvar $n) $h ↪ dbcongT tvar (aux_teq_shift_shift_var $i $j $n $h)
with aux_teq_shift_shift _ _ (tuniv _) _ ↪ TRefl _
with aux_teq_shift_shift _ _ (tpi $A $B) $h ↪
Jpi (aux_teq_shift_shift _ _ $A $h)
(aux_teq_shift_shift _ _ $B (dble_n_S $h))
with aux_teq_shift_shift _ _ (tabs $A $t) $h ↪
Jabs (aux_teq_shift_shift _ _ $A $h)
(aux_teq_shift_shift _ _ $t (dble_n_S $h))
with aux_teq_shift_shift _ _ (tapp $f $a) $h ↪
Japp (aux_teq_shift_shift _ _ $f $h)
(aux_teq_shift_shift _ _ $a $h)
with aux_teq_shift_shift _ _ tnat _ ↪ TRefl _
with aux_teq_shift_shift _ _ tzero _ ↪ TRefl _
with aux_teq_shift_shift _ _ (tsuc $n) $h ↪ Jcong tsuc (aux_teq_shift_shift _ _ $n $h)
with aux_teq_shift_shift _ _ (trec $P $z $H $n) $h ↪
Jrec (aux_teq_shift_shift _ _ $P $h)
(aux_teq_shift_shift _ _ $z $h)
(aux_teq_shift_shift _ _ $H $h)
(aux_teq_shift_shift _ _ $n $h)
with aux_teq_shift_shift _ _ (tsig $A $B) $h ↪
Jsig (aux_teq_shift_shift _ _ $A $h)
(aux_teq_shift_shift _ _ $B (dble_n_S $h))
with aux_teq_shift_shift _ _ (tpair $a $b) $h ↪
Jpair (aux_teq_shift_shift _ _ $a $h)
(aux_teq_shift_shift _ _ $b $h)
with aux_teq_shift_shift _ _ (tp1 $p) $h ↪
Jcong tp1 (aux_teq_shift_shift _ _ $p $h)
with aux_teq_shift_shift _ _ (tp2 $p) $h ↪
Jcong tp2 (aux_teq_shift_shift _ _ $p $h)
with aux_teq_shift_shift _ _ (tsum $A $B) $h ↪
Jsum (aux_teq_shift_shift _ _ $A $h)
(aux_teq_shift_shift _ _ $B $h)
with aux_teq_shift_shift _ _ (tinjl $p) $h ↪
Jcong tinjl (aux_teq_shift_shift _ _ $p $h)
with aux_teq_shift_shift _ _ (tinjr $p) $h ↪
Jcong tinjr (aux_teq_shift_shift _ _ $p $h)
with aux_teq_shift_shift _ _ (tcase $P $A $B $Ha $Hb $n) $h ↪
Jcase (aux_teq_shift_shift _ _ $P $h)
(aux_teq_shift_shift _ _ $A $h)
(aux_teq_shift_shift _ _ $B $h)
(aux_teq_shift_shift _ _ $Ha $h)
(aux_teq_shift_shift _ _ $Hb $h)
(aux_teq_shift_shift _ _ $n $h)
with aux_teq_shift_shift _ _ (tpath $A $x $y) $h ↪
Jpath (aux_teq_shift_shift _ _ $A $h)
(aux_teq_shift_shift _ _ $x $h)
(aux_teq_shift_shift _ _ $y $h)
with aux_teq_shift_shift _ _ (tlamP $t) $h ↪
Jcong tlamP (aux_teq_shift_shift _ _ $t $h)
with aux_teq_shift_shift _ _ (tappP $u _) $h ↪
JappP (aux_teq_shift_shift _ _ $u $h) (ITRefl _)
with aux_teq_shift_shift _ _ (tsys _ _ $u $v) $h ↪
Jsys (FTRefl _) (FTRefl _)
(aux_teq_shift_shift _ _ $u $h)
(aux_teq_shift_shift _ _ $v $h)
with aux_teq_shift_shift _ _ temptysys _ ↪ TRefl _
with aux_teq_shift_shift _ _ (ttransp $A _ $u) $h ↪
Jtransp (aux_teq_shift_shift _ _ $A $h)
(FTRefl _)
(aux_teq_shift_shift _ _ $u $h)
with aux_teq_shift_shift _ _ (thcomp $A _ $u $v) $h ↪
Jhcomp (aux_teq_shift_shift _ _ $A $h)
(FTRefl _)
(aux_teq_shift_shift _ _ $u $h)
(aux_teq_shift_shift _ _ $v $h);
// teq_Ishift_Ishift
symbol aux_teq_Ishift_Ishift (i j : DBId) (u : Term) :
DBLe i j → TEq (Ishift i (Ishift j u)) (Ishift (dbsucc j) (Ishift i u));
symbol aux_teq_IshiftI_IshiftI (i j : DBId) (u : ITerm) :
DBLe i j → ITEq (IshiftI i (IshiftI j u)) (IshiftI (dbsucc j) (IshiftI i u));
symbol aux_teq_IshiftF_IshiftF (i j : DBId) (u : FTerm) :
DBLe i j → FTEq (IshiftF i (IshiftF j u)) (IshiftF (dbsucc j) (IshiftF i u));
rule aux_teq_Ishift_Ishift _ _ (tvar _) _ ↪ TRefl _
with aux_teq_Ishift_Ishift _ _ (tuniv _) _ ↪ TRefl _
with aux_teq_Ishift_Ishift _ _ (tpi $A $B) $h ↪
Jpi (aux_teq_Ishift_Ishift _ _ $A $h)
(aux_teq_Ishift_Ishift _ _ $B $h)
with aux_teq_Ishift_Ishift _ _ (tabs $A $B) $h ↪
Jabs (aux_teq_Ishift_Ishift _ _ $A $h)
(aux_teq_Ishift_Ishift _ _ $B $h)
with aux_teq_Ishift_Ishift _ _ (tapp $A $B) $h ↪
Japp (aux_teq_Ishift_Ishift _ _ $A $h)
(aux_teq_Ishift_Ishift _ _ $B $h)
with aux_teq_Ishift_Ishift _ _ tnat _ ↪ TRefl _
with aux_teq_Ishift_Ishift _ _ tzero _ ↪ TRefl _
with aux_teq_Ishift_Ishift _ _ (tsuc $s) $h ↪
Jcong tsuc (aux_teq_Ishift_Ishift _ _ $s $h)
with aux_teq_Ishift_Ishift _ _ (trec $P $z $H $n) $h ↪
Jrec (aux_teq_Ishift_Ishift _ _ $P $h)
(aux_teq_Ishift_Ishift _ _ $z $h)
(aux_teq_Ishift_Ishift _ _ $H $h)
(aux_teq_Ishift_Ishift _ _ $n $h)
with aux_teq_Ishift_Ishift _ _ (tsig $A $B) $h ↪
Jsig (aux_teq_Ishift_Ishift _ _ $A $h)
(aux_teq_Ishift_Ishift _ _ $B $h)
with aux_teq_Ishift_Ishift _ _ (tpair $A $B) $h ↪
Jpair (aux_teq_Ishift_Ishift _ _ $A $h)
(aux_teq_Ishift_Ishift _ _ $B $h)
with aux_teq_Ishift_Ishift _ _ (tp1 $s) $h ↪
Jcong tp1 (aux_teq_Ishift_Ishift _ _ $s $h)
with aux_teq_Ishift_Ishift _ _ (tp2 $s) $h ↪
Jcong tp2 (aux_teq_Ishift_Ishift _ _ $s $h)
with aux_teq_Ishift_Ishift _ _ (tsum $A $B) $h ↪
Jsum (aux_teq_Ishift_Ishift _ _ $A $h)
(aux_teq_Ishift_Ishift _ _ $B $h)
with aux_teq_Ishift_Ishift _ _ (tinjl $s) $h ↪
Jcong tinjl (aux_teq_Ishift_Ishift _ _ $s $h)
with aux_teq_Ishift_Ishift _ _ (tinjr $s) $h ↪
Jcong tinjr (aux_teq_Ishift_Ishift _ _ $s $h)
with aux_teq_Ishift_Ishift _ _ (tcase $P $A $B $Ha $Hb $t) $h ↪
Jcase (aux_teq_Ishift_Ishift _ _ $P $h)
(aux_teq_Ishift_Ishift _ _ $A $h)
(aux_teq_Ishift_Ishift _ _ $B $h)
(aux_teq_Ishift_Ishift _ _ $Ha $h)
(aux_teq_Ishift_Ishift _ _ $Hb $h)
(aux_teq_Ishift_Ishift _ _ $t $h)
with aux_teq_Ishift_Ishift _ _ (tpath $A $x $y) $h ↪
Jpath (aux_teq_Ishift_Ishift _ _ $A (dble_n_S $h))
(aux_teq_Ishift_Ishift _ _ $x $h)
(aux_teq_Ishift_Ishift _ _ $y $h)
with aux_teq_Ishift_Ishift _ _ (tlamP $s) $h ↪
Jcong tlamP (aux_teq_Ishift_Ishift _ _ $s (dble_n_S $h))
with aux_teq_Ishift_Ishift _ _ (tappP $u $v) $h ↪
JappP (aux_teq_Ishift_Ishift _ _ $u $h)
(aux_teq_IshiftI_IshiftI _ _ $v $h)
with aux_teq_Ishift_Ishift _ _ (tsys $f $g $u $v) $h ↪
Jsys (aux_teq_IshiftF_IshiftF _ _ $f $h)
(aux_teq_IshiftF_IshiftF _ _ $g $h)
(aux_teq_Ishift_Ishift _ _ $u $h)
(aux_teq_Ishift_Ishift _ _ $v $h)
with aux_teq_Ishift_Ishift _ _ temptysys _ ↪ TRefl _
with aux_teq_Ishift_Ishift _ _ (ttransp $A $f $u) $h ↪
Jtransp (aux_teq_Ishift_Ishift _ _ $A (dble_n_S $h))
(aux_teq_IshiftF_IshiftF _ _ $f $h)
(aux_teq_Ishift_Ishift _ _ $u $h)
with aux_teq_Ishift_Ishift _ _ (thcomp $A $f $u $v) $h ↪
Jhcomp (aux_teq_Ishift_Ishift _ _ $A $h)
(aux_teq_IshiftF_IshiftF _ _ $f $h)
(aux_teq_Ishift_Ishift _ _ $u (dble_n_S $h))
(aux_teq_Ishift_Ishift _ _ $v $h)
with aux_teq_IshiftI_IshiftI _ _ it0 _ ↪ ITRefl _
with aux_teq_IshiftI_IshiftI _ _ it1 _ ↪ ITRefl _
with aux_teq_IshiftI_IshiftI _ _ (itvar $id) $h ↪
dbcongI itvar (aux_teq_shift_shift_var _ _ $id $h)
with aux_teq_IshiftI_IshiftI _ _ (itsym $i) $h ↪
IJcong itsym (aux_teq_IshiftI_IshiftI _ _ $i $h)
with aux_teq_IshiftI_IshiftI _ _ (itmin $i $j) $h ↪
IJmin (aux_teq_IshiftI_IshiftI _ _ $i $h)
(aux_teq_IshiftI_IshiftI _ _ $j $h)
with aux_teq_IshiftI_IshiftI _ _ (itmax $i $j) $h ↪
IJmax (aux_teq_IshiftI_IshiftI _ _ $i $h)
(aux_teq_IshiftI_IshiftI _ _ $j $h)
with aux_teq_IshiftF_IshiftF _ _ ft0 _ ↪ FTRefl _
with aux_teq_IshiftF_IshiftF _ _ ft1 _ ↪ FTRefl _
with aux_teq_IshiftF_IshiftF _ _ (fteq0 $id) $h ↪
dbcongF fteq0 (aux_teq_shift_shift_var _ _ $id $h)
with aux_teq_IshiftF_IshiftF _ _ (fteq1 $id) $h ↪
dbcongF fteq1 (aux_teq_shift_shift_var _ _ $id $h)
with aux_teq_IshiftF_IshiftF _ _ (ftmin $i $j) $h ↪
FJmin (aux_teq_IshiftF_IshiftF _ _ $i $h)
(aux_teq_IshiftF_IshiftF _ _ $j $h)
with aux_teq_IshiftF_IshiftF _ _ (ftmax $i $j) $h ↪
FJmax (aux_teq_IshiftF_IshiftF _ _ $i $h)
(aux_teq_IshiftF_IshiftF _ _ $j $h);
// teq_shift_shift0
symbol aux_teq_shift_shift0 (i : DBId) (u : Term) :
TEq (Shift (shift i u)) (shift (dbsucc i) (Shift u)) ≔
aux_teq_shift_shift db0 i u (dble_0_n i);
symbol aux_teq_Ishift_Ishift0 (i : DBId) (u : Term) :
TEq (IShift (Ishift i u)) (Ishift (dbsucc i) (IShift u)) ≔
aux_teq_Ishift_Ishift db0 i u (dble_0_n i);
symbol aux_teq_IshiftI_IshiftI0 (i : DBId) (u : ITerm) :
ITEq (IShiftI (IshiftI i u)) (IshiftI (dbsucc i) (IShiftI u)) ≔
aux_teq_IshiftI_IshiftI db0 i u (dble_0_n i);
// teq_shift_shiftI
symbol aux_teq_shift_Ishift (i j : DBId) (u : Term) :
TEq (shift i (Ishift j u)) (Ishift j (shift i u));
rule aux_teq_shift_Ishift _ _ (tvar _) ↪ TRefl _
with aux_teq_shift_Ishift _ _ (tuniv _) ↪ TRefl _
with aux_teq_shift_Ishift $i $j (tpi $A $B) ↪
Jpi (aux_teq_shift_Ishift $i $j $A)
(aux_teq_shift_Ishift (dbsucc $i) $j $B)
with aux_teq_shift_Ishift $i $j (tabs $A $t) ↪
Jabs (aux_teq_shift_Ishift $i $j $A)
(aux_teq_shift_Ishift (dbsucc $i) $j $t)
with aux_teq_shift_Ishift $i $j (tapp $f $a) ↪
Japp (aux_teq_shift_Ishift $i $j $f)
(aux_teq_shift_Ishift $i $j $a)
with aux_teq_shift_Ishift _ _ tnat ↪ TRefl _
with aux_teq_shift_Ishift _ _ tzero ↪ TRefl _
with aux_teq_shift_Ishift $i $j (tsuc $n) ↪
Jcong tsuc (aux_teq_shift_Ishift $i $j $n)
with aux_teq_shift_Ishift $i $j (trec $P $z $H $n) ↪
Jrec (aux_teq_shift_Ishift $i $j $P)
(aux_teq_shift_Ishift $i $j $z)
(aux_teq_shift_Ishift $i $j $H)
(aux_teq_shift_Ishift $i $j $n)
with aux_teq_shift_Ishift $i $j (tsig $A $B) ↪
Jsig (aux_teq_shift_Ishift $i $j $A)
(aux_teq_shift_Ishift (dbsucc $i) $j $B)
with aux_teq_shift_Ishift $i $j (tpair $a $b) ↪
Jpair (aux_teq_shift_Ishift $i $j $a)
(aux_teq_shift_Ishift $i $j $b)
with aux_teq_shift_Ishift $i $j (tp1 $p) ↪
Jcong tp1 (aux_teq_shift_Ishift $i $j $p)
with aux_teq_shift_Ishift $i $j (tp2 $p) ↪
Jcong tp2 (aux_teq_shift_Ishift $i $j $p)
with aux_teq_shift_Ishift $i $j (tsum $A $B) ↪
Jsum (aux_teq_shift_Ishift $i $j $A)
(aux_teq_shift_Ishift $i $j $B)
with aux_teq_shift_Ishift $i $j (tinjl $p) ↪
Jcong tinjl (aux_teq_shift_Ishift $i $j $p)
with aux_teq_shift_Ishift $i $j (tinjr $p) ↪
Jcong tinjr (aux_teq_shift_Ishift $i $j $p)
with aux_teq_shift_Ishift $i $j (tcase $P $A $B $Ha $Hb $n) ↪
Jcase (aux_teq_shift_Ishift $i $j $P)
(aux_teq_shift_Ishift $i $j $A)
(aux_teq_shift_Ishift $i $j $B)
(aux_teq_shift_Ishift $i $j $Ha)
(aux_teq_shift_Ishift $i $j $Hb)
(aux_teq_shift_Ishift $i $j $n)
with aux_teq_shift_Ishift $i $j (tpath $A $x $y) ↪
Jpath (aux_teq_shift_Ishift $i (dbsucc $j) $A)
(aux_teq_shift_Ishift $i $j $x)
(aux_teq_shift_Ishift $i $j $y)
with aux_teq_shift_Ishift $i $j (tlamP $t) ↪
Jcong tlamP (aux_teq_shift_Ishift $i (dbsucc $j) $t)
with aux_teq_shift_Ishift $i $j (tappP $u _) ↪
JappP (aux_teq_shift_Ishift $i $j $u) (ITRefl _)
with aux_teq_shift_Ishift $i $j (tsys _ _ $u $v) ↪
Jsys (FTRefl _) (FTRefl _)
(aux_teq_shift_Ishift $i $j $u)
(aux_teq_shift_Ishift $i $j $v)
with aux_teq_shift_Ishift _ _ temptysys ↪ TRefl _
with aux_teq_shift_Ishift $i $j (ttransp $A _ $u) ↪
Jtransp (aux_teq_shift_Ishift $i (dbsucc $j) $A)
(FTRefl _)
(aux_teq_shift_Ishift $i $j $u)
with aux_teq_shift_Ishift $i $j (thcomp $A _ $u $v) ↪
Jhcomp (aux_teq_shift_Ishift $i $j $A)
(FTRefl _)
(aux_teq_shift_Ishift $i (dbsucc $j) $u)
(aux_teq_shift_Ishift $i $j $v);
symbol aux_teq_Shift*_Ishift (i j : DBId) (u : Term) :
TEq (Shift* i (Ishift j u)) (Ishift j (Shift* i u));
rule aux_teq_Shift*_Ishift db0 _ _ ↪ TRefl _
with aux_teq_Shift*_Ishift (dbsucc $i) $j $u ↪
teq_trans (Jcong Shift (aux_teq_Shift*_Ishift $i $j $u)) (aux_teq_shift_Ishift db0 $j (Shift* $i $u));
// teq_shift_dbselect
symbol aux_teq_shift_dbselect (n i j : DBId) (eqT gtT ltT : Term) :
TEq (shift n (dbselect i j eqT gtT ltT))
(dbselect i j (shift n eqT) (shift n gtT) (shift n ltT));
rule aux_teq_shift_dbselect $n db0 db0 $eqT _ _ ↪ TRefl (shift $n $eqT)
with aux_teq_shift_dbselect $n (dbsucc _) db0 _ $gtT _ ↪ TRefl (shift $n $gtT)
with aux_teq_shift_dbselect $n db0 (dbsucc _) _ _ $ltT ↪ TRefl (shift $n $ltT)
with aux_teq_shift_dbselect $n (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT ↪
aux_teq_shift_dbselect $n $i $j $eqT $gtT $ltT;
// teq_shift_dbselect0
symbol aux_teq_shift_dbselect0 (i j : DBId) (eqT gtT ltT : Term) :
TEq (Shift (dbselect i j eqT gtT ltT))
(dbselect i j (Shift eqT) (Shift gtT) (Shift ltT)) ≔
aux_teq_shift_dbselect db0 i j eqT gtT ltT;
// teq_Ishift_dbselect
symbol aux_teq_Ishift_dbselect (n i j : DBId) (eqT gtT ltT : Term) :
TEq (Ishift n (dbselect i j eqT gtT ltT))
(dbselect i j (Ishift n eqT) (Ishift n gtT) (Ishift n ltT));
rule aux_teq_Ishift_dbselect $n db0 db0 $eqT _ _ ↪ TRefl (Ishift $n $eqT)
with aux_teq_Ishift_dbselect $n (dbsucc _) db0 _ $gtT _ ↪ TRefl (Ishift $n $gtT)
with aux_teq_Ishift_dbselect $n db0 (dbsucc _) _ _ $ltT ↪ TRefl (Ishift $n $ltT)
with aux_teq_Ishift_dbselect $n (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT ↪
aux_teq_Ishift_dbselect $n $i $j $eqT $gtT $ltT;
// teq_shift_dbselect0
symbol aux_teq_Ishift_dbselect0 (i j : DBId) (eqT gtT ltT : Term) :
TEq (IShift (dbselect i j eqT gtT ltT))
(dbselect i j (IShift eqT) (IShift gtT) (IShift ltT)) ≔
aux_teq_Ishift_dbselect db0 i j eqT gtT ltT;
// teq_shift_dbselectI
symbol aux_teq_shift_dbselectI (n i j : DBId) (eqT gtT ltT : ITerm) :
ITEq (IshiftI n (dbselectI i j eqT gtT ltT))
(dbselectI i j (IshiftI n eqT) (IshiftI n gtT) (IshiftI n ltT));
rule aux_teq_shift_dbselectI _ db0 db0 _ _ _ ↪ ITRefl _
with aux_teq_shift_dbselectI _ (dbsucc _) db0 _ _ _ ↪ ITRefl _
with aux_teq_shift_dbselectI _ db0 (dbsucc _) _ _ _ ↪ ITRefl _
with aux_teq_shift_dbselectI $n (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT ↪
aux_teq_shift_dbselectI $n $i $j $eqT $gtT $ltT;
// teq_shift_dbselectI0
symbol aux_teq_shift_dbselectI0 (i j : DBId) (eqT gtT ltT : ITerm) :
ITEq (IShiftI (dbselectI i j eqT gtT ltT))
(dbselectI i j (IShiftI eqT) (IShiftI gtT) (IShiftI ltT)) ≔
aux_teq_shift_dbselectI db0 i j eqT gtT ltT;
// teq_shift_dbselectF
symbol aux_teq_shift_dbselectF (n i j : DBId) (eqT gtT ltT : FTerm) :
FTEq (IshiftF n (dbselectF i j eqT gtT ltT))
(dbselectF i j (IshiftF n eqT) (IshiftF n gtT) (IshiftF n ltT));
rule aux_teq_shift_dbselectF _ db0 db0 _ _ _ ↪ FTRefl _
with aux_teq_shift_dbselectF _ (dbsucc _) db0 _ _ _ ↪ FTRefl _
with aux_teq_shift_dbselectF _ db0 (dbsucc _) _ _ _ ↪ FTRefl _
with aux_teq_shift_dbselectF $n (dbsucc $i) (dbsucc $j) $eqT $gtT $ltT ↪
aux_teq_shift_dbselectF $n $i $j $eqT $gtT $ltT;
// teq_shift_dbselectF0
symbol aux_teq_shift_dbselectF0 (i j : DBId) (eqT gtT ltT : FTerm) :
FTEq (IShiftF (dbselectF i j eqT gtT ltT))
(dbselectF i j (IShiftF eqT) (IShiftF gtT) (IShiftF ltT)) ≔
aux_teq_shift_dbselectF db0 i j eqT gtT ltT;
// teq_dbselect_fn
symbol aux_teq_dbselect_fn (i n : DBId) (eqT gtT : Term) (f : DBId → Term) :
TEq (dbselect i n eqT gtT (f n))
(dbselect i n eqT gtT (f (dbsucc (dbprev n))));
rule aux_teq_dbselect_fn db0 db0 $eqT _ _ ↪ TRefl $eqT
with aux_teq_dbselect_fn (dbsucc _) db0 _ $gtT _ ↪ TRefl $gtT
with aux_teq_dbselect_fn db0 (dbsucc $n) _ _ $f ↪ TRefl ($f (dbsucc $n))
with aux_teq_dbselect_fn (dbsucc $i) (dbsucc $n) $eqT $gtT $f ↪ TRefl (dbselect $i $n $eqT $gtT ($f (dbsucc $n)));
// teq_dbselect_Sn
symbol aux_teq_dbselect_Sn (i n : DBId) (eqT gtT : Term) :
TEq (dbselect i n eqT gtT (tvar n))
(dbselect i n eqT gtT (tvar (dbsucc (dbprev n)))) ≔
aux_teq_dbselect_fn i n eqT gtT tvar;
// teq_dbselectI_fn
symbol aux_teq_dbselectI_fn (i n : DBId) (eqT gtT : ITerm) (f : DBId → ITerm) :
ITEq (dbselectI i n eqT gtT (f n))
(dbselectI i n eqT gtT (f (dbsucc (dbprev n))));
rule aux_teq_dbselectI_fn db0 db0 $eqT _ _ ↪ ITRefl $eqT
with aux_teq_dbselectI_fn (dbsucc _) db0 _ $gtT _ ↪ ITRefl $gtT
with aux_teq_dbselectI_fn db0 (dbsucc $n) _ _ $f ↪ ITRefl ($f (dbsucc $n))
with aux_teq_dbselectI_fn (dbsucc $i) (dbsucc $n) $eqT $gtT $f ↪ ITRefl (dbselectI $i $n $eqT $gtT ($f (dbsucc $n)));
// teq_dbselect_Sn
symbol aux_teq_dbselectI_Sn (i n : DBId) (eqT gtT : ITerm) :
ITEq (dbselectI i n eqT gtT (itvar n))
(dbselectI i n eqT gtT (itvar (dbsucc (dbprev n)))) ≔
aux_teq_dbselectI_fn i n eqT gtT itvar;
// teq_dbselectF_fn
symbol aux_teq_dbselectF_fn (i n : DBId) (eqT gtT : FTerm) (f : DBId → FTerm) :
FTEq (dbselectF i n eqT gtT (f n))
(dbselectF i n eqT gtT (f (dbsucc (dbprev n))));
rule aux_teq_dbselectF_fn db0 db0 $eqT _ _ ↪ FTRefl $eqT
with aux_teq_dbselectF_fn (dbsucc _) db0 _ $gtT _ ↪ FTRefl $gtT
with aux_teq_dbselectF_fn db0 (dbsucc $n) _ _ $f ↪ FTRefl ($f (dbsucc $n))
with aux_teq_dbselectF_fn (dbsucc $i) (dbsucc $n) $eqT $gtT $f ↪ FTRefl (dbselectF $i $n $eqT $gtT ($f (dbsucc $n)));
// teq_dbselectF_Sn0
symbol aux_teq_dbselectF_Sn0 (i n : DBId) (eqT gtT : FTerm) :
FTEq (dbselectF i n eqT gtT (fteq0 n))
(dbselectF i n eqT gtT (fteq0 (dbsucc (dbprev n)))) ≔
aux_teq_dbselectF_fn i n eqT gtT fteq0;
// teq_dbselectF_Sn1
symbol aux_teq_dbselectF_Sn1 (i n : DBId) (eqT gtT : FTerm) :
FTEq (dbselectF i n eqT gtT (fteq1 n))
(dbselectF i n eqT gtT (fteq1 (dbsucc (dbprev n)))) ≔
aux_teq_dbselectF_fn i n eqT gtT fteq1;
// teq_shift_substeq*
symbol aux_teq_Ishift_substeq0 (i : DBId) (u : ITerm) :
FTEq (substeq0 (IshiftI i u)) (IshiftF i (substeq0 u));
symbol aux_teq_Ishift_substeq1 (i : DBId) (u : ITerm) :
FTEq (substeq1 (IshiftI i u)) (IshiftF i (substeq1 u));
rule aux_teq_Ishift_substeq0 _ it0 ↪ FTRefl _
with aux_teq_Ishift_substeq0 _ it1 ↪ FTRefl _
with aux_teq_Ishift_substeq0 _ (itvar _) ↪ FTRefl _
with aux_teq_Ishift_substeq0 $i (itsym $u) ↪ aux_teq_Ishift_substeq1 $i $u
with aux_teq_Ishift_substeq0 $i (itmin $x $y) ↪
FJmax (aux_teq_Ishift_substeq0 $i $x)
(aux_teq_Ishift_substeq0 $i $y)
with aux_teq_Ishift_substeq0 $i (itmax $x $y) ↪
FJmin (aux_teq_Ishift_substeq0 $i $x)
(aux_teq_Ishift_substeq0 $i $y)
with aux_teq_Ishift_substeq1 _ it0 ↪ FTRefl _
with aux_teq_Ishift_substeq1 _ it1 ↪ FTRefl _
with aux_teq_Ishift_substeq1 _ (itvar _) ↪ FTRefl _
with aux_teq_Ishift_substeq1 $i (itsym $u) ↪ aux_teq_Ishift_substeq0 $i $u
with aux_teq_Ishift_substeq1 $i (itmin $x $y) ↪
FJmin (aux_teq_Ishift_substeq1 $i $x)
(aux_teq_Ishift_substeq1 $i $y)
with aux_teq_Ishift_substeq1 $i (itmax $x $y) ↪
FJmax (aux_teq_Ishift_substeq1 $i $x)
(aux_teq_Ishift_substeq1 $i $y);
symbol aux_teq_IShift*_substeq0 (i : DBId) (u : ITerm) :
FTEq (substeq0 (IShiftI* i u)) (IShiftF* i (substeq0 u));
symbol aux_teq_IShift*_substeq1 (i : DBId) (u : ITerm) :
FTEq (substeq1 (IShiftI* i u)) (IShiftF* i (substeq1 u));
rule aux_teq_IShift*_substeq0 db0 _ ↪ FTRefl _
with aux_teq_IShift*_substeq0 (dbsucc $i) $u ↪
fteq_trans (aux_teq_Ishift_substeq0 db0 (IShiftI* $i $u))
(FJcong IShiftF (aux_teq_IShift*_substeq0 $i $u))
with aux_teq_IShift*_substeq1 db0 _ ↪ FTRefl _
with aux_teq_IShift*_substeq1 (dbsucc $i) $u ↪
fteq_trans (aux_teq_Ishift_substeq1 db0 (IShiftI* $i $u))
(FJcong IShiftF (aux_teq_IShift*_substeq1 $i $u));
// teq_select_substeq*
symbol aux_teq_select_substeq0 (i j : DBId) (eq gt lt : ITerm) :
FTEq (substeq0 (dbselectI i j eq gt lt)) (dbselectF i j (substeq0 eq) (substeq0 gt) (substeq0 lt));
rule aux_teq_select_substeq0 db0 db0 $eq _ _ ↪ FTRefl (substeq0 $eq)
with aux_teq_select_substeq0 (dbsucc _) db0 _ $gt _ ↪ FTRefl (substeq0 $gt)
with aux_teq_select_substeq0 db0 (dbsucc _) _ _ $lt ↪ FTRefl (substeq0 $lt)
with aux_teq_select_substeq0 (dbsucc $i) (dbsucc $j) $eq $gt $lt ↪
aux_teq_select_substeq0 $i $j $eq $gt $lt;
symbol aux_teq_select_substeq1 (i j : DBId) (eq gt lt : ITerm) :
FTEq (substeq1 (dbselectI i j eq gt lt)) (dbselectF i j (substeq1 eq) (substeq1 gt) (substeq1 lt));
rule aux_teq_select_substeq1 db0 db0 $eq _ _ ↪ FTRefl (substeq1 $eq)
with aux_teq_select_substeq1 (dbsucc _) db0 _ $gt _ ↪ FTRefl (substeq1 $gt)
with aux_teq_select_substeq1 db0 (dbsucc _) _ _ $lt ↪ FTRefl (substeq1 $lt)
with aux_teq_select_substeq1 (dbsucc $i) (dbsucc $j) $eq $gt $lt ↪
aux_teq_select_substeq1 $i $j $eq $gt $lt;
// teq_subst_substeq*
symbol aux_teq_Isubst_substeq0 (i : DBId) (t u : ITerm) :
FTEq (substeq0 (IsubstI i t u)) (IsubstF i t (substeq0 u));
symbol aux_teq_Isubst_substeq1 (i : DBId) (t u : ITerm) :
FTEq (substeq1 (IsubstI i t u)) (IsubstF i t (substeq1 u));
rule aux_teq_Isubst_substeq0 _ _ it0 ↪ FTRefl _
with aux_teq_Isubst_substeq0 _ _ it1 ↪ FTRefl _
with aux_teq_Isubst_substeq0 $i $t (itvar $j) ↪
aux_teq_select_substeq0 $i $j $t (itvar $j) (itvar (dbprev $j))
with aux_teq_Isubst_substeq0 $i $t (itsym $u) ↪ aux_teq_Isubst_substeq1 $i $t $u
with aux_teq_Isubst_substeq0 $i $t (itmin $x $y) ↪
FJmax (aux_teq_Isubst_substeq0 $i $t $x)
(aux_teq_Isubst_substeq0 $i $t $y)
with aux_teq_Isubst_substeq0 $i $t (itmax $x $y) ↪
FJmin (aux_teq_Isubst_substeq0 $i $t $x)
(aux_teq_Isubst_substeq0 $i $t $y)
with aux_teq_Isubst_substeq1 _ _ it0 ↪ FTRefl _
with aux_teq_Isubst_substeq1 _ _ it1 ↪ FTRefl _
with aux_teq_Isubst_substeq1 $i $t (itvar $j) ↪
aux_teq_select_substeq1 $i $j $t (itvar $j) (itvar (dbprev $j))
with aux_teq_Isubst_substeq1 $i $t (itsym $u) ↪ aux_teq_Isubst_substeq0 $i $t $u
with aux_teq_Isubst_substeq1 $i $t (itmin $x $y) ↪
FJmin (aux_teq_Isubst_substeq1 $i $t $x)
(aux_teq_Isubst_substeq1 $i $t $y)
with aux_teq_Isubst_substeq1 $i $t (itmax $x $y) ↪
FJmax (aux_teq_Isubst_substeq1 $i $t $x)
(aux_teq_Isubst_substeq1 $i $t $y);
// teq_subst_shift
symbol aux_teq_subst_shift (i j : DBId) (u t : Term) :
DBLe j i →
TEq (subst (dbsucc i) (shift j (Shift* j u)) (shift j t))
(shift j (subst i (Shift* j u) t));
// teq_subst_shift_var
symbol aux_teq_subst_shift_var (i j : DBId) (u : Term) (n : DBId) :
DBLe j i →
TEq (dbselect (dbsucc i) (dbshift j n) (shift j (Shift* j u)) (tvar (dbshift j n)) (tvar (dbprev (dbshift j n))))
(dbselect i n (shift j (Shift* j u)) (tvar (dbshift j n)) (tvar (dbshift j (dbprev n))));
symbol aux_teq_subst_shift_Ishift (i j : DBId) (u t : Term) (h : DBLe j i) :
TEq (subst (dbsucc i) (IShift (shift j (Shift* j u))) (shift j t))
(shift j (subst i (IShift (Shift* j u)) t)) ≔
teq_trans (Jcong (λ u1, subst (dbsucc i) u1 (shift j t))
(teq_inv (aux_teq_shift_Ishift j db0 (Shift* j u))))
(teq_trans (Jcong (λ u1, subst (dbsucc i) (shift j u1) (shift j t))
(teq_inv (aux_teq_Shift*_Ishift j db0 u)))
(teq_trans (aux_teq_subst_shift i j (IShift u) t h)
(Jcong (λ u1, shift j (subst i u1 t))
(aux_teq_Shift*_Ishift j db0 u))));
rule aux_teq_subst_shift_var $i db0 $u $n _ ↪
aux_teq_dbselect_Sn $i $n (shift db0 $u) (tvar (dbsucc $n))
with aux_teq_subst_shift_var (dbsucc _) (dbsucc _) _ db0 _ ↪
TRefl (tvar db0)
with aux_teq_subst_shift_var (dbsucc db0) (dbsucc $j) $u (dbsucc db0) $h ↪
teq_trans
(teq_trans
(aux_teq_dbselect_Sn (dbsucc db0) (dbshift $j db0) (shift (dbsucc $j) (Shift* (dbsucc $j) $u))
(tvar (dbsucc (dbshift $j db0))))
(teq_inv (aux_teq_shift_dbselect0 (dbsucc db0) (dbshift $j db0) (shift $j (Shift* $j $u))
(tvar (dbshift $j db0)) (tvar (dbprev (dbshift $j db0))))))
(teq_trans
(Jcong Shift (aux_teq_subst_shift_var db0 $j $u db0 (dble_S_n $h)))
(aux_teq_shift_dbselect0 db0 db0 (shift $j (Shift* $j $u)) (tvar (dbshift $j db0))
(tvar (dbshift $j (dbprev db0)))))
with aux_teq_subst_shift_var (dbsucc (dbsucc $i)) (dbsucc $j) $u (dbsucc db0) $h ↪
teq_trans
(teq_trans
(aux_teq_dbselect_Sn (dbsucc (dbsucc $i)) (dbshift $j db0) (shift (dbsucc $j) (Shift* (dbsucc $j) $u))
(tvar (dbsucc (dbshift $j db0))))
(teq_inv (aux_teq_shift_dbselect0 (dbsucc (dbsucc $i)) (dbshift $j db0) (shift $j (Shift* $j $u))
(tvar (dbshift $j db0)) (tvar (dbprev (dbshift $j db0))))))
(teq_trans
(Jcong Shift (aux_teq_subst_shift_var (dbsucc $i) $j $u db0 (dble_S_n $h)))
(aux_teq_shift_dbselect0 (dbsucc $i) db0 (shift $j (Shift* $j $u))
(tvar (dbshift $j db0)) (tvar (dbshift $j (dbprev db0)))))
with aux_teq_subst_shift_var (dbsucc $i) (dbsucc $j) $u (dbsucc (dbsucc $n)) $h ↪
teq_trans
(teq_trans
(aux_teq_dbselect_Sn (dbsucc $i) (dbshift $j (dbsucc $n)) (shift (dbsucc $j) (Shift* (dbsucc $j) $u))
(tvar (dbsucc (dbshift $j (dbsucc $n)))))
(teq_inv (aux_teq_shift_dbselect0 (dbsucc $i) (dbshift $j (dbsucc $n)) (shift $j (Shift* $j $u))
(tvar (dbshift $j (dbsucc $n)))
(tvar (dbprev (dbshift $j (dbsucc $n)))))))
(teq_trans
(Jcong Shift (aux_teq_subst_shift_var $i $j $u (dbsucc $n) (dble_S_n $h)))
(aux_teq_shift_dbselect0 $i (dbsucc $n) (shift $j (Shift* $j $u))
(tvar (dbshift $j (dbsucc $n))) (tvar (dbshift $j ($n)))));
rule aux_teq_subst_shift $i $j $u (tvar $n) $h ↪
teq_trans
(aux_teq_subst_shift_var $i $j $u $n $h)
(teq_inv (aux_teq_shift_dbselect $j $i $n (Shift* $j $u) (tvar $n) (tvar (dbprev $n))))
with aux_teq_subst_shift _ _ _ (tuniv _) _ ↪ TRefl _
with aux_teq_subst_shift $i $j $u (tpi $A $B) $h ↪
Jpi (aux_teq_subst_shift $i $j $u $A $h)
(aux_teq_subst_shift (dbsucc $i) (dbsucc $j) $u $B (dble_n_S $h))
with aux_teq_subst_shift $i $j $u (tabs $A $t) $h ↪
Jabs (aux_teq_subst_shift $i $j $u $A $h)
(aux_teq_subst_shift (dbsucc $i) (dbsucc $j) $u $t (dble_n_S $h))
with aux_teq_subst_shift $i $j $u (tapp $f $a) $h ↪
Japp (aux_teq_subst_shift $i $j $u $f $h)
(aux_teq_subst_shift $i $j $u $a $h)
with aux_teq_subst_shift _ _ _ tnat _ ↪ TRefl _
with aux_teq_subst_shift _ _ _ tzero _ ↪ TRefl _
with aux_teq_subst_shift $i $j $u (tsuc $n) $h ↪
Jcong tsuc (aux_teq_subst_shift $i $j $u $n $h)
with aux_teq_subst_shift $i $j $u (trec $P $z $H $n) $h ↪
Jrec (aux_teq_subst_shift $i $j $u $P $h)
(aux_teq_subst_shift $i $j $u $z $h)
(aux_teq_subst_shift $i $j $u $H $h)
(aux_teq_subst_shift $i $j $u $n $h)
with aux_teq_subst_shift $i $j $u (tsig $A $B) $h ↪
Jsig (aux_teq_subst_shift $i $j $u $A $h)
(aux_teq_subst_shift (dbsucc $i) (dbsucc $j) $u $B (dble_n_S $h))
with aux_teq_subst_shift $i $j $u (tpair $a $b) $h ↪
Jpair (aux_teq_subst_shift $i $j $u $a $h)
(aux_teq_subst_shift $i $j $u $b $h)
with aux_teq_subst_shift $i $j $u (tp1 $p) $h ↪
Jcong tp1 (aux_teq_subst_shift $i $j $u $p $h)
with aux_teq_subst_shift $i $j $u (tp2 $p) $h ↪
Jcong tp2 (aux_teq_subst_shift $i $j $u $p $h)
with aux_teq_subst_shift $i $j $u (tsum $A $B) $h ↪
Jsum (aux_teq_subst_shift $i $j $u $A $h)
(aux_teq_subst_shift $i $j $u $B $h)
with aux_teq_subst_shift $i $j $u (tinjl $p) $h ↪
Jcong tinjl (aux_teq_subst_shift $i $j $u $p $h)
with aux_teq_subst_shift $i $j $u (tinjr $p) $h ↪
Jcong tinjr (aux_teq_subst_shift $i $j $u $p $h)
with aux_teq_subst_shift $i $j $u (tcase $A $B $P $a $b $t) $h ↪
Jcase (aux_teq_subst_shift $i $j $u $A $h)
(aux_teq_subst_shift $i $j $u $B $h)
(aux_teq_subst_shift $i $j $u $P $h)
(aux_teq_subst_shift $i $j $u $a $h)
(aux_teq_subst_shift $i $j $u $b $h)
(aux_teq_subst_shift $i $j $u $t $h)
with aux_teq_subst_shift $i $j $u (tpath $A $x $y) $h ↪
Jpath (aux_teq_subst_shift_Ishift $i $j $u $A $h)