-lemma cpm_tdeq_ind (a) (h) (o) (n) (G) (Q:relation3 …):
- (∀I,L. n = 0 → Q L (⓪{I}) (⓪{I})) →
- (∀L,s. n = 1 → deg h o s 0 → Q L (⋆s) (⋆(next h s))) →
- (∀p,I,L,V,T1. ⦃G,L⦄⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T1![a,h] →
- ∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 →
- Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
- ) →
- (∀m. (a = Ⓣ → m ≤ 1) →
- ∀L,V. ⦃G,L⦄ ⊢ V ![a,h] → ∀W. ⦃G, L⦄ ⊢ V ➡*[1,h] W →
- ∀p,T1,U1. ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![a,h] →
- ∀T2. ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 →
- Q L T1 T2 → Q L (ⓐV.T1) (ⓐV.T2)
- ) →
- (∀L,U0,U1,T1. ⦃G,L⦄ ⊢ U1 ➡*[h] U0 → ⦃G,L⦄ ⊢ T1 ➡*[1,h] U0 →
- ∀U2. ⦃G, L⦄ ⊢ U1 ![a,h] → ⦃G, L⦄ ⊢ U1 ➡[n,h] U2 → U1 ≛[h,o] U2 →
- ∀T2. ⦃G, L⦄ ⊢ T1 ![a,h] → ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 →
- Q L U1 U2 → Q L T1 T2 → Q L (ⓝU1.T1) (ⓝU2.T2)
- ) →
- ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
- ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → Q L T1 T2.
-#a #h #o #n #G #Q #IH1 #IH2 #IH3 #IH4 #IH5 #L #T1
+lemma cpm_tdeq_ind (h) (a) (n) (G) (Q:relation3 …):
+ (∀I,L. n = 0 → Q L (⓪{I}) (⓪{I})) →
+ (∀L,s. n = 1 → Q L (⋆s) (⋆(⫯[h]s))) →
+ (∀p,I,L,V,T1. ⦃G,L⦄⊢ V![h,a] → ⦃G,L.ⓑ{I}V⦄⊢T1![h,a] →
+ ∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →
+ Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
+ ) →
+ (∀m. ad a m →
+ ∀L,V. ⦃G,L⦄ ⊢ V ![h,a] → ∀W. ⦃G,L⦄ ⊢ V ➡*[1,h] W →
+ ∀p,T1,U1. ⦃G,L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![h,a] →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →
+ Q L T1 T2 → Q L (ⓐV.T1) (ⓐV.T2)
+ ) →
+ (∀L,U0,U1,T1. ⦃G,L⦄ ⊢ U1 ➡*[h] U0 → ⦃G,L⦄ ⊢ T1 ➡*[1,h] U0 →
+ ∀U2. ⦃G,L⦄ ⊢ U1 ![h,a] → ⦃G,L⦄ ⊢ U1 ➡[n,h] U2 → U1 ≛ U2 →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ![h,a] → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →
+ Q L U1 U2 → Q L T1 T2 → Q L (ⓝU1.T1) (ⓝU2.T2)
+ ) →
+ ∀L,T1. ⦃G,L⦄ ⊢ T1 ![h,a] →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → Q L T1 T2.
+#h #a #n #G #Q #IH1 #IH2 #IH3 #IH4 #IH5 #L #T1