(* Advanced eliminators *****************************************************)
lemma tc_lfxs_ind_sn: ∀R. c_reflexive … R →
- ∀L1,T. ∀R0:predicate …. R0 L1 →
- (∀L,L2. L1 ⪤**[R, T] L → L ⪤*[R, T] L2 → R0 L → R0 L2) →
- ∀L2. L1 ⪤**[R, T] L2 → R0 L2.
-#R #HR #L1 #T #R0 #HL1 #IHL1 #L2 #HL12
+ ∀L1,T. ∀Q:predicate …. Q L1 →
+ (∀L,L2. L1 ⪤**[R, T] L → L ⪤*[R, T] L2 → Q L → Q L2) →
+ ∀L2. L1 ⪤**[R, T] L2 → Q L2.
+#R #HR #L1 #T #Q #HL1 #IHL1 #L2 #HL12
@(TC_star_ind … HL1 IHL1 … HL12) /2 width=1 by lfxs_refl/
qed-.
lemma tc_lfxs_ind_dx: ∀R. c_reflexive … R →
- ∀L2,T. ∀R0:predicate …. R0 L2 →
- (∀L1,L. L1 ⪤*[R, T] L → L ⪤**[R, T] L2 → R0 L → R0 L1) →
- ∀L1. L1 ⪤**[R, T] L2 → R0 L1.
-#R #HR #L2 #R0 #HL2 #IHL2 #L1 #HL12
+ ∀L2,T. ∀Q:predicate …. Q L2 →
+ (∀L1,L. L1 ⪤*[R, T] L → L ⪤**[R, T] L2 → Q L → Q L1) →
+ ∀L1. L1 ⪤**[R, T] L2 → Q L1.
+#R #HR #L2 #Q #HL2 #IHL2 #L1 #HL12
@(TC_star_ind_dx … HL2 IHL2 … HL12) /2 width=4 by lfxs_refl/
qed-.
I,J : item
K,L : local environment
M,N : reserved: future use
-O,P,Q :
-R : generic predicate (relation)
+O :
+P : relocation environment
+Q : elimination predicate
+R : generic predicate/relation
S : RTM stack
T,U,V,W: term
X,Y,Z : reserved: transient objet denoted by a capital letter
/2 width=9 by lexs_trans_gen/ qed-.
theorem lexs_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤*[R1, cfull, f] L → 𝐈⦃f⦄ →
- ∀L2. L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2.
+ ∀L2. L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2.
#R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f
[ #f #Hf #L2 #H >(lexs_inv_atom1 … H) -L2 // ]
#f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H
Q 0 T2 →
(∀n1,n2,T1,T. ⦃G, L⦄ ⊢ T1 ➡[n1, h] T → ⦃G, L⦄ ⊢ T ➡*[n2, h] T2 → Q n2 T → Q (n1+n2) T1) →
∀n,T1. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → Q n T1.
-#h #G #L #T2 #R @ltc_ind_sn_refl //
+#h #G #L #T2 #Q @ltc_ind_sn_refl //
qed-.
lemma cpms_ind_dx (h) (G) (L) (T1) (Q:relation2 …):
Q 0 T1 →
(∀n1,n2,T,T2. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T → Q n1 T → ⦃G, L⦄ ⊢ T ➡[n2, h] T2 → Q (n1+n2) T2) →
∀n,T2. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → Q n T2.
-#h #G #L #T1 #R @ltc_ind_dx_refl //
+#h #G #L #T1 #Q @ltc_ind_dx_refl //
qed-.
(* Basic inversion lemmas ***************************************************)
(* Basic eliminators ********************************************************)
(* Basic_2A1: was: cprs_ind_dx *)
-lemma cprs_ind_sn (h) (G) (L) (T2) (R:predicate …):
- R T2 →
- (∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ⦃G, L⦄ ⊢ T ➡*[h] T2 → R T → R T1) →
- ∀T1. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → R T1.
-#h #G #L #T2 #R #IH1 #IH2 #T1
+lemma cprs_ind_sn (h) (G) (L) (T2) (Q:predicate …):
+ Q T2 →
+ (∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ⦃G, L⦄ ⊢ T ➡*[h] T2 → Q T → Q T1) →
+ ∀T1. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → Q T1.
+#h #G #L #T2 #Q #IH1 #IH2 #T1
@(insert_eq_0 … 0) #n #H
@(cpms_ind_sn … H) -n -T1 //
#n1 #n2 #T1 #T #HT1 #HT2 #IH #H
qed-.
(* Basic_2A1: was: cprs_ind *)
-lemma cprs_ind_dx (h) (G) (L) (T1) (R:predicate …):
- R T1 →
- (∀T,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T → ⦃G, L⦄ ⊢ T ➡[h] T2 → R T → R T2) →
- ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → R T2.
-#h #G #L #T1 #R #IH1 #IH2 #T2
+lemma cprs_ind_dx (h) (G) (L) (T1) (Q:predicate …):
+ Q T1 →
+ (∀T,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T → ⦃G, L⦄ ⊢ T ➡[h] T2 → Q T → Q T2) →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → Q T2.
+#h #G #L #T1 #Q #IH1 #IH2 #T2
@(insert_eq_0 … 0) #n #H
@(cpms_ind_dx … H) -n -T2 //
#n1 #n2 #T #T2 #HT1 #IH #HT2 #H
(* Basic eliminators ********************************************************)
-lemma cpxs_ind: ∀h,G,L,T1. ∀R:predicate term. R T1 →
- (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ T ⬈[h] T2 → R T → R T2) →
- ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T2.
-#h #L #G #T1 #R #HT1 #IHT1 #T2 #HT12
+lemma cpxs_ind: ∀h,G,L,T1. ∀Q:predicate term. Q T1 →
+ (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ T ⬈[h] T2 → Q T → Q T2) →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → Q T2.
+#h #L #G #T1 #Q #HT1 #IHT1 #T2 #HT12
@(TC_star_ind … HT1 IHT1 … HT12) //
qed-.
-lemma cpxs_ind_dx: ∀h,G,L,T2. ∀R:predicate term. R T2 →
- (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T → ⦃G, L⦄ ⊢ T ⬈*[h] T2 → R T → R T1) →
- ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T1.
-#h #G #L #T2 #R #HT2 #IHT2 #T1 #HT12
+lemma cpxs_ind_dx: ∀h,G,L,T2. ∀Q:predicate term. Q T2 →
+ (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T → ⦃G, L⦄ ⊢ T ⬈*[h] T2 → Q T → Q T1) →
+ ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → Q T1.
+#h #G #L #T2 #Q #HT2 #IHT2 #T1 #HT12
@(TC_star_ind_dx … HT2 IHT2 … HT12) //
qed-.
(* Basic eliminators ********************************************************)
-lemma csx_ind: ∀h,o,G,L. ∀R:predicate term.
+lemma csx_ind: ∀h,o,G,L. ∀Q:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) →
- R T1
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) →
+ Q T1
) →
- ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
-#h #o #G #L #R #H0 #T1 #H elim H -T1
+ ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → Q T.
+#h #o #G #L #Q #H0 #T1 #H elim H -T1
/5 width=1 by SN_intro/
qed-.
(* Advanced eliminators *****************************************************)
-fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term.
+fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀Q:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
) →
- ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
+ ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → Q T.
+#h #o #G #L #A #Q #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
qed-.
-lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term.
+lemma aaa_ind_csx: ∀h,o,G,L,A. ∀Q:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
) →
- ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
+ ∀T. ⦃G, L⦄ ⊢ T ⁝ A → Q T.
/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
-fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term.
+fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀Q:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
) →
- ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
+ ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → Q T.
+#h #o #G #L #A #Q #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
qed-.
(* Basic_2A1: was: aaa_ind_csx_alt *)
-lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term.
+lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀Q:predicate term.
(∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
) →
- ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
+ ∀T. ⦃G, L⦄ ⊢ T ⁝ A → Q T.
/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-.
(* Eliminators with unbound context-sensitive rt-computation for terms ******)
-lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀R:predicate term.
+lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀Q:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
) →
∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- ∀T0. ⦃G, L⦄ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛[h, o] T2 → R T2.
-#h #o #G #L #R #IH #T1 #H @(csx_ind … H) -T1
+ ∀T0. ⦃G, L⦄ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛[h, o] T2 → Q T2.
+#h #o #G #L #Q #IH #T1 #H @(csx_ind … H) -T1
#T1 #HT1 #IH1 #T0 #HT10 #T2 #HT02
@IH -IH /3 width=3 by csx_cpxs_trans, csx_tdeq_trans/ -HT1 #V2 #HTV2 #HnTV2
lapply (tdeq_tdneq_trans … HT02 … HnTV2) -HnTV2 #H
qed-.
(* Basic_2A1: was: csx_ind_alt *)
-lemma csx_ind_cpxs: ∀h,o,G,L. ∀R:predicate term.
+lemma csx_ind_cpxs: ∀h,o,G,L. ∀Q:predicate term.
(∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+ (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
) →
- ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
-#h #o #G #L #R #IH #T #HT
+ ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → Q T.
+#h #o #G #L #Q #IH #T #HT
@(csx_ind_cpxs_tdeq … IH … HT) -IH -HT // (**) (* full auto fails *)
qed-.
(* Basic eliminators ********************************************************)
-lemma fpbs_ind: ∀h,o,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 →
- (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+lemma fpbs_ind: ∀h,o,G1,L1,T1. ∀Q:relation3 genv lenv term. Q G1 L1 T1 →
+ (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
/3 width=8 by tri_TC_star_ind/ qed-.
-lemma fpbs_ind_dx: ∀h,o,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 →
- (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
- ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G1 L1 T1.
+lemma fpbs_ind_dx: ∀h,o,G2,L2,T2. ∀Q:relation3 genv lenv term. Q G2 L2 T2 →
+ (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G1 L1 T1.
/3 width=8 by tri_TC_star_ind_dx/ qed-.
(* Basic properties *********************************************************)
(* Note: eliminator with shorter ground hypothesis *)
(* Note: to be named fsb_ind when fsb becomes a definition like csx, lfsx ***)
-lemma fsb_ind_alt: ∀h,o. ∀R: relation3 …. (
+lemma fsb_ind_alt: ∀h,o. ∀Q: relation3 …. (
∀G1,L1,T1. ≥[h,o] 𝐒⦃G1, L1, T1⦄ → (
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2
- ) → R G1 L1 T1
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2
+ ) → Q G1 L1 T1
) →
- ∀G,L,T. ≥[h, o] 𝐒⦃G, L, T⦄ → R G L T.
-#h #o #R #IH #G #L #T #H elim H -G -L -T
+ ∀G,L,T. ≥[h, o] 𝐒⦃G, L, T⦄ → Q G L T.
+#h #o #Q #IH #G #L #T #H elim H -G -L -T
/4 width=1 by fsb_intro/
qed-.
(* Advanced eliminators with atomic arity assignment for terms **************)
-fact aaa_ind_fpb_aux: ∀h,o. ∀R:relation3 ….
+fact aaa_ind_fpb_aux: ∀h,o. ∀Q:relation3 ….
(∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
) →
- ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T.
#h #o #R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T
#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
#G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h o … G2 … L2 … T2 … HTA1) -A1
/2 width=2 by fpb_fpbs/
qed-.
-lemma aaa_ind_fpb: ∀h,o. ∀R:relation3 ….
+lemma aaa_ind_fpb: ∀h,o. ∀Q:relation3 ….
(∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
) →
- ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+ ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T.
/4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-.
-fact aaa_ind_fpbg_aux: ∀h,o. ∀R:relation3 ….
+fact aaa_ind_fpbg_aux: ∀h,o. ∀Q:relation3 ….
(∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
) →
- ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
-#h #o #R #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T.
+#h #o #Q #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T
#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
#G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h o … G2 … L2 … T2 … HTA1) -A1
/2 width=2 by fpbg_fwd_fpbs/
qed-.
-lemma aaa_ind_fpbg: ∀h,o. ∀R:relation3 ….
+lemma aaa_ind_fpbg: ∀h,o. ∀Q:relation3 ….
(∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
) →
- ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+ ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T.
/4 width=4 by aaa_ind_fpbg_aux, aaa_csx/ qed-.
(* Advanced eliminators *****************************************************)
-lemma csx_ind_fpb: ∀h,o. ∀R:relation3 genv lenv term.
+lemma csx_ind_fpb: ∀h,o. ∀Q:relation3 genv lenv term.
(∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
) →
- ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R G L T.
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → Q G L T.
/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
-lemma csx_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term.
+lemma csx_ind_fpbg: ∀h,o. ∀Q:relation3 genv lenv term.
(∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
) →
- ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R G L T.
+ ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → Q G L T.
/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-.
(* Eliminators with proper parallel rst-computation for closures ************)
-lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀R:relation3 genv lenv term.
+lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀Q:relation3 genv lenv term.
(∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
) →
∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#h #o #R #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
+#h #o #Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
#G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
@IH1 -IH1
[ -IH /2 width=5 by fsb_fpbs_trans/
]
qed-.
-lemma fsb_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term.
+lemma fsb_ind_fpbg: ∀h,o. ∀Q:relation3 genv lenv term.
(∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
) →
- ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → R G1 L1 T1.
-#h #o #R #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
+ ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → Q G1 L1 T1.
+#h #o #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
/3 width=1 by/
qed-.
(* Basic eliminators ********************************************************)
(* Basic_2A1: was: lprs_ind_alt *)
-lemma lprs_ind (h) (G): ∀R:relation lenv.
- R (⋆) (⋆) → (
+lemma lprs_ind (h) (G): ∀Q:relation lenv.
+ Q (⋆) (⋆) → (
∀I,K1,K2.
⦃G, K1⦄ ⊢ ➡*[h] K2 →
- R K1 K2 → R (K1.ⓘ{I}) (K2.ⓘ{I})
+ Q K1 K2 → Q (K1.ⓘ{I}) (K2.ⓘ{I})
) → (
∀I,K1,K2,V1,V2.
⦃G, K1⦄ ⊢ ➡*[h] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h] V2 →
- R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ Q K1 K2 → Q (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
) →
- ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1 L2.
+ ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L1 L2.
/3 width=4 by lex_ind/ qed-.
(* Eliminators with r-transition for full local environments ****************)
(* Basic_2A1: was: lprs_ind_dx *)
-lemma lprs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 →
- (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → ⦃G, L⦄ ⊢ ➡*[h] L2 → R L → R L1) →
- ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1.
+lemma lprs_ind_sn (h) (G) (L2): ∀Q:predicate lenv. Q L2 →
+ (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → ⦃G, L⦄ ⊢ ➡*[h] L2 → Q L → Q L1) →
+ ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L1.
/4 width=8 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, cpr_refl, lex_CTC_ind_sn/ qed-.
(* Basic_2A1: was: lprs_ind *)
-lemma lprs_ind_dx (h) (G) (L1): ∀R:predicate lenv. R L1 →
- (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h] L → ⦃G, L⦄ ⊢ ➡[h] L2 → R L → R L2) →
- ∀L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L2.
+lemma lprs_ind_dx (h) (G) (L1): ∀Q:predicate lenv. Q L1 →
+ (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h] L → ⦃G, L⦄ ⊢ ➡[h] L2 → Q L → Q L2) →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L2.
/4 width=8 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, cpr_refl, lex_CTC_ind_dx/ qed-.
(* Properties with unbound rt-transition for full local environments ********)
(* Basic eliminators ********************************************************)
(* Basic_2A1: was: lpxs_ind_alt *)
-lemma lpxs_ind (h) (G): ∀R:relation lenv.
- R (⋆) (⋆) → (
+lemma lpxs_ind (h) (G): ∀Q:relation lenv.
+ Q (⋆) (⋆) → (
∀I,K1,K2.
⦃G, K1⦄ ⊢ ⬈*[h] K2 →
- R K1 K2 → R (K1.ⓘ{I}) (K2.ⓘ{I})
+ Q K1 K2 → Q (K1.ⓘ{I}) (K2.ⓘ{I})
) → (
∀I,K1,K2,V1,V2.
⦃G, K1⦄ ⊢ ⬈*[h] K2 → ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 →
- R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ Q K1 K2 → Q (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
) →
- ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L1 L2.
+ ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → Q L1 L2.
/3 width=4 by lex_ind/ qed-.
(* Eliminators with unbound rt-transition for full local environments *******)
(* Basic_2A1: was: lpxs_ind_dx *)
-lemma lpxs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 →
- (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → ⦃G, L⦄ ⊢ ⬈*[h] L2 → R L → R L1) →
- ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L1.
+lemma lpxs_ind_sn (h) (G) (L2): ∀Q:predicate lenv. Q L2 →
+ (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → ⦃G, L⦄ ⊢ ⬈*[h] L2 → Q L → Q L1) →
+ ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → Q L1.
/3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_sn/ qed-.
(* Basic_2A1: was: lpxs_ind *)
-lemma lpxs_ind_dx (h) (G) (L1): ∀R:predicate lenv. R L1 →
- (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L → ⦃G, L⦄ ⊢ ⬈[h] L2 → R L → R L2) →
- ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L2.
+lemma lpxs_ind_dx (h) (G) (L1): ∀Q:predicate lenv. Q L1 →
+ (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L → ⦃G, L⦄ ⊢ ⬈[h] L2 → Q L → Q L2) →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → Q L2.
/3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_dx/ qed-.
(* Properties with context-sensitive extended rt-transition for terms *******)
(* Basic_2A1: uses: lsx_ind *)
lemma rdsx_ind (h) (o) (G) (T):
- ∀R:predicate lenv.
+ ∀Q:predicate lenv.
(∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
- R L1
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) →
+ Q L1
) →
- ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
-#h #o #G #T #R #H0 #L1 #H elim H -L1
+ ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → Q L.
+#h #o #G #T #Q #H0 #L1 #H elim H -L1
/5 width=1 by SN_intro/
qed-.
(* Eliminators with unbound rt-computation for full local environments ******)
lemma rdsx_ind_lpxs_lfdeq (h) (o) (G):
- ∀T. ∀R:predicate lenv.
+ ∀T. ∀Q:predicate lenv.
(∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
- R L1
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) →
+ Q L1
) →
∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → R L2.
-#h #o #G #T #R #IH #L1 #H @(rdsx_ind … H) -L1
+ ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → Q L2.
+#h #o #G #T #Q #IH #L1 #H @(rdsx_ind … H) -L1
#L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02
@IH -IH /3 width=3 by rdsx_lpxs_trans, rdsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2
lapply (lfdeq_lfdneq_trans … HL02 … HnLK2) -HnLK2 #H
(* Basic_2A1: uses: lsx_ind_alt *)
lemma rdsx_ind_lpxs (h) (o) (G):
- ∀T. ∀R:predicate lenv.
+ ∀T. ∀Q:predicate lenv.
(∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
- (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
- R L1
+ (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) →
+ Q L1
) →
- ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
-#h #o #G #T #R #IH #L #HL
+ ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → Q L.
+#h #o #G #T #Q #IH #L #HL
@(rdsx_ind_lpxs_lfdeq … IH … HL) -IH -HL // (**) (* full auto fails *)
qed-.
(* Basic_2A1: was: cpcs_ind_dx *)
lemma cpcs_ind_sn (h) (G) (L) (T2):
- ∀R:predicate term. R T2 →
- (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) →
- ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1.
+ ∀Q:predicate term. Q T2 →
+ (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → Q T → Q T1) →
+ ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → Q T1.
normalize /3 width=6 by TC_star_ind_dx/
qed-.
(* Basic_2A1: was: cpcs_ind *)
lemma cpcs_ind_dx (h) (G) (L) (T1):
- ∀R:predicate term. R T1 →
- (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) →
- ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2.
+ ∀Q:predicate term. Q T1 →
+ (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → Q T → Q T2) →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → Q T2.
normalize /3 width=6 by TC_star_ind/
qed-.
(* Basic eliminators ********************************************************)
-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)
) → (∀n,p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 →
- R 0 G L V1 V2 → R n G (L.ⓑ{I}V1) T1 T2 → R n G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+ Q 0 G L V1 V2 → Q n G (L.ⓑ{I}V1) T1 T2 → Q n G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
) → (∀n,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
- R 0 G L V1 V2 → R n G L T1 T2 → R n G L (ⓐV1.T1) (ⓐV2.T2)
+ Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2)
) → (∀n,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
- R n G L V1 V2 → R n G L T1 T2 → R n G L (ⓝV1.T1) (ⓝV2.T2)
- ) → (∀n,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T → R n G (L.ⓓV) T1 T →
- ⬆*[1] T2 ≘ T → R n G L (+ⓓV.T1) T2
+ Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2)
+ ) → (∀n,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T → Q n G (L.ⓓV) T1 T →
+ ⬆*[1] T2 ≘ T → Q n G L (+ⓓV.T1) T2
) → (∀n,G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
- R n G L T1 T2 → R n G L (ⓝV.T1) T2
+ Q n G L T1 T2 → Q n G L (ⓝV.T1) T2
) → (∀n,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 →
- R n G L V1 V2 → R (↑n) G L (ⓝV1.T) V2
+ Q n G L V1 V2 → Q (↑n) G L (ⓝV1.T) V2
) → (∀n,p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 →
- R 0 G L V1 V2 → R 0 G L W1 W2 → R n G (L.ⓛW1) T1 T2 →
- R n G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+ Q 0 G L V1 V2 → Q 0 G L W1 W2 → Q n G (L.ⓛW1) T1 T2 →
+ Q n G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
) → (∀n,p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 →
- R 0 G L V1 V → R 0 G L W1 W2 → R n G (L.ⓓW1) T1 T2 →
- ⬆*[1] V ≘ V2 → R n G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+ Q 0 G L V1 V → Q 0 G L W1 W2 → Q n G (L.ⓓW1) T1 T2 →
+ ⬆*[1] V ≘ V2 → Q n G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
) →
- ∀n,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → R n G L T1 T2.
-#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #IH12 #IH13 #n #G #L #T1 #T2
+ ∀n,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → Q n G L T1 T2.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #IH12 #IH13 #n #G #L #T1 #T2
* #c #HC #H generalize in match HC; -HC generalize in match n; -n
elim H -c -G -L -T1 -T2
[ #I #G #L #n #H <(isrt_inv_00 … H) -H //
(* Basic eliminators ********************************************************)
-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)
) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[h] T2 →
- R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+ Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 →
- R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
- ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → R G (L.ⓓV) T1 T →
- ⬆*[1] T2 ≘ T → R G L (+ⓓV.T1) T2
- ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2 →
- R G L (ⓝV.T1) T2
+ Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+ ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → Q G (L.ⓓV) T1 T →
+ ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2
+ ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L T1 T2 →
+ Q G L (ⓝV.T1) T2
) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h] T2 →
- R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 →
- R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+ Q G L V1 V2 → Q G L W1 W2 → Q G (L.ⓛW1) T1 T2 →
+ Q G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h] T2 →
- R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 →
- ⬆*[1] V ≘ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+ Q G L V1 V → Q G L W1 W2 → Q G (L.ⓓW1) T1 T2 →
+ ⬆*[1] V ≘ V2 → Q G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
) →
- ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2.
-#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2
+ ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L T1 T2.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2
@(insert_eq_0 … 0) #n #H
@(cpm_ind … H) -G -L -T1 -T2 -n /3 width=4 by/
[ #G #L #s #H destruct
(* Basic eliminators ********************************************************)
-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)
) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
- R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+ Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
- R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
- ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → R G (L.ⓓV) T1 T →
- ⬆*[1] T2 ≘ T → R G L (+ⓓV.T1) T2
- ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2 →
- R G L (ⓝV.T1) T2
- ) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → R G L V1 V2 →
- R G L (ⓝV1.T) V2
+ Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+ ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → Q G (L.ⓓV) T1 T →
+ ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2
+ ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → Q G L T1 T2 →
+ Q G L (ⓝV.T1) T2
+ ) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → Q G L V1 V2 →
+ Q G L (ⓝV1.T) V2
) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 →
- R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 →
- R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+ Q G L V1 V2 → Q G L W1 W2 → Q G (L.ⓛW1) T1 T2 →
+ Q G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 →
- R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 →
- ⬆*[1] V ≘ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+ Q G L V1 V → Q G L W1 W2 → Q G (L.ⓓW1) T1 T2 →
+ ⬆*[1] V ≘ V2 → Q G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
) →
- ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2.
-#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #G #L #T1 #T2
+ ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → Q G L T1 T2.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #G #L #T1 #T2
* #c #H elim H -c -G -L -T1 -T2 /3 width=4 by ex_intro/
qed-.
(* Basic eliminators ********************************************************)
-lemma fqup_ind: ∀b,G1,L1,T1. ∀R:relation3 ….
- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#b #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
+lemma fqup_ind: ∀b,G1,L1,T1. ∀Q:relation3 ….
+ (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
+#b #G1 #L1 #T1 #Q #IH1 #IH2 #G2 #L2 #T2 #H
@(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
qed-.
-lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀R:relation3 ….
- (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G1 L1 T1) →
- (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
- ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G1 L1 T1.
-#b #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 ….
+ (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1) →
+ (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1.
+#b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H
@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
qed-.
(* Advanced eliminators *****************************************************)
-lemma fqup_wf_ind: ∀b. ∀R:relation3 …. (
- ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
- ) → ∀G1,L1,T1. R G1 L1 T1.
-#b #R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
+lemma fqup_wf_ind: ∀b. ∀Q:relation3 …. (
+ ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) → ∀G1,L1,T1. Q G1 L1 T1.
+#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
/4 width=2 by fqup_fwd_fw/
qed-.
-lemma fqup_wf_ind_eq: ∀b. ∀R:relation3 …. (
- ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2
- ) → ∀G1,L1,T1. R G1 L1 T1.
-#b #R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
+lemma fqup_wf_ind_eq: ∀b. ∀Q:relation3 …. (
+ ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → Q G2 L2 T2
+ ) → ∀G1,L1,T1. Q G1 L1 T1.
+#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
/4 width=7 by fqup_fwd_fw/
qed-.
(* Basic eliminators ********************************************************)
-lemma fqus_ind: ∀b,G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 →
- (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+lemma fqus_ind: ∀b,G1,L1,T1. ∀Q:relation3 …. Q G1 L1 T1 →
+ (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
#b #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
@(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) //
qed-.
-lemma fqus_ind_dx: ∀b,G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 →
- (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐*[b] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
- ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → R G1 L1 T1.
-#b #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+lemma fqus_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 …. Q G2 L2 T2 →
+ (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐*[b] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1.
+#b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H
@(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) //
qed-.
(* Advanced eliminators *****************************************************)
-lemma fqu_wf_ind: ∀b. ∀R:relation3 …. (
- ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
- R G1 L1 T1
- ) → ∀G1,L1,T1. R G1 L1 T1.
-#b #R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/
+lemma fqu_wf_ind: ∀b. ∀Q:relation3 …. (
+ ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+ Q G1 L1 T1
+ ) → ∀G1,L1,T1. Q G1 L1 T1.
+#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/
qed-.
]
qed-.
-lemma frees_ind_void: ∀R:relation3 ….
+lemma frees_ind_void: ∀Q:relation3 ….
(
- ∀f,L,s. 𝐈⦃f⦄ → R L (⋆s) f
+ ∀f,L,s. 𝐈⦃f⦄ → Q L (⋆s) f
) → (
- ∀f,i. 𝐈⦃f⦄ → R (⋆) (#i) (⫯*[i]↑f)
+ ∀f,i. 𝐈⦃f⦄ → Q (⋆) (#i) (⫯*[i]↑f)
) → (
∀f,I,L,V.
- L ⊢ 𝐅*⦃V⦄ ≘ f → R L V f→ R (L.ⓑ{I}V) (#O) (↑f)
+ L ⊢ 𝐅*⦃V⦄ ≘ f → Q L V f→ Q (L.ⓑ{I}V) (#O) (↑f)
) → (
- ∀f,I,L. 𝐈⦃f⦄ → R (L.ⓤ{I}) (#O) (↑f)
+ ∀f,I,L. 𝐈⦃f⦄ → Q (L.ⓤ{I}) (#O) (↑f)
) → (
∀f,I,L,i.
- L ⊢ 𝐅*⦃#i⦄ ≘ f → R L (#i) f → R (L.ⓘ{I}) (#(↑i)) (⫯f)
+ L ⊢ 𝐅*⦃#i⦄ ≘ f → Q L (#i) f → Q (L.ⓘ{I}) (#(↑i)) (⫯f)
) → (
- ∀f,L,l. 𝐈⦃f⦄ → R L (§l) f
+ ∀f,L,l. 𝐈⦃f⦄ → Q L (§l) f
) → (
∀f1,f2,f,p,I,L,V,T.
L ⊢ 𝐅*⦃V⦄ ≘ f1 → L.ⓧ ⊢𝐅*⦃T⦄≘ f2 → f1 ⋓ ⫱f2 ≘ f →
- R L V f1 →R (L.ⓧ) T f2 → R L (ⓑ{p,I}V.T) f
+ Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ{p,I}V.T) f
) → (
∀f1,f2,f,I,L,V,T.
L ⊢ 𝐅*⦃V⦄ ≘ f1 → L ⊢𝐅*⦃T⦄ ≘ f2 → f1 ⋓ f2 ≘ f →
- R L V f1 → R L T f2 → R L (ⓕ{I}V.T) f
+ Q L V f1 → Q L T f2 → Q L (ⓕ{I}V.T) f
) →
- ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≘ f → R L T f.
-#R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
+ ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≘ f → Q L T f.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
@(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * *
[ #s #HG #HL #HT #f #H destruct -IH
lapply (frees_inv_sort … H) -H /2 width=1 by/
/4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed.
lemma lfxs_lref (R): ∀I1,I2,L1,L2,i.
- L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #↑i] L2.ⓘ{I2}.
+ L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #↑i] L2.ⓘ{I2}.
#R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/
qed.
∃∃L2. L1 ⪤*[R, U] L2 & ⬇*[b, f] L2 ≘ K2 & L1 ≡[f] L2.
definition f_dropable_sn: predicate (relation3 lenv term term) ≝
- λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ →
- ∀L2,U. L1 ⪤*[R, U] L2 → ∀T. ⬆*[f] T ≘ U →
- ∃∃K2. K1 ⪤*[R, T] K2 & ⬇*[b, f] L2 ≘ K2.
+ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ →
+ ∀L2,U. L1 ⪤*[R, U] L2 → ∀T. ⬆*[f] T ≘ U →
+ ∃∃K2. K1 ⪤*[R, T] K2 & ⬇*[b, f] L2 ≘ K2.
definition f_dropable_dx: predicate (relation3 lenv term term) ≝
λR. ∀L1,L2,U. L1 ⪤*[R, U] L2 →
(* Basic_1: was: c_tail_ind *)
(* Basic_2A1: was: lenv_ind_alt *)
-lemma lenv_ind_tail: ∀R:predicate lenv.
- R (⋆) → (∀I,L. R L → R (ⓘ{I}.L)) → ∀L. R L.
-#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * //
+lemma lenv_ind_tail: ∀Q:predicate lenv.
+ Q (⋆) → (∀I,L. Q L → Q (ⓘ{I}.L)) → ∀L. Q L.
+#Q #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * //
#L #I -IH1 #H destruct
elim (lenv_case_tail … L) [2: * #K #J ]
#H destruct /3 width=1 by/