-lemma cpx_ind: ∀h. ∀R:relation4 genv lenv term term.
- (∀I,G,L. R G L (⓪{I}) (⓪{I})) →
- (∀G,L,s. R G L (⋆s) (⋆(next h s))) →
- (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → R G K V1 V2 →
- ⬆*[1] V2 ≘ W2 → R G (K.ⓑ{I}V1) (#0) W2
- ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T →
- ⬆*[1] T ≘ U → R G (K.ⓘ{I}) (#↑i) (U)
+lemma cpx_ind: ∀h. ∀Q:relation4 genv lenv term term.
+ (∀I,G,L. Q G L (⓪{I}) (⓪{I})) →
+ (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+ (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → Q G K V1 V2 →
+ ⬆*[1] V2 ≘ W2 → Q G (K.ⓑ{I}V1) (#0) W2
+ ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → Q G K (#i) T →
+ ⬆*[1] T ≘ U → Q G (K.ⓘ{I}) (#↑i) (U)