#G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e
[ //
| #I #G #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) -HL12 -HLK1 /3 width=7 by cpysa_subst/
+ elim (lsuby_ldrop_trans_be … HL12 … HLK1) -HL12 -HLK1 /3 width=7 by cpysa_subst/
| /4 width=1 by lsuby_succ, cpysa_bind/
| /3 width=1 by cpysa_flat/
]
(* Basic inversion lemmas ***************************************************)
-lemma cpysa_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2.
+lemma cpysa_inv_cpys: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2.
#G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e
/2 width=7 by cpys_subst, cpys_flat, cpys_bind, cpy_cpys/
qed-.
+(* Advanced eliminators *****************************************************)
+
lemma cpys_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term.
(∀I,G,L,d,e. R d e G L (⓪{I}) (⓪{I})) →
(∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e →
) →
∀d,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 → R d e G L T1 T2.
#R #H1 #H2 #H3 #H4 #d #e #G #L #T1 #T2 #H elim (cpys_cpysa … H) -G -L -T1 -T2 -d -e
-/3 width=8 by cpysa_cpys/
+/3 width=8 by cpysa_inv_cpys/
qed-.