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