-lemma cpr_ind (h): ∀R:relation4 genv lenv term term.
- (∀I,G,L. R G L (⓪{I}) (⓪{I})) →
- (∀G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 → R G K V1 V2 →
- ⬆*[1] V2 ≘ W2 → R G (K.ⓓ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 cpr_ind (h): ∀Q:relation4 genv lenv term term.
+ (∀I,G,L. Q G L (⓪{I}) (⓪{I})) →
+ (∀G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 → Q G K V1 V2 →
+ ⬆*[1] V2 ≘ W2 → Q G (K.ⓓ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)