+
+(* Advanced eliminators *****************************************************)
+
+lemma lleq_ind_alt: ∀R:relation4 ynat term lenv lenv. (
+ ∀L1,L2,d,k. |L1| = |L2| → R d (⋆k) L1 L2
+ ) → (
+ ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2
+ ) → (
+ ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V →
+ K1 ⋕[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
+ ) → (
+ ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2
+ ) → (
+ ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2
+ ) → (
+ ∀a,I,L1,L2,V,T,d.
+ L1 ⋕[V, d]L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V →
+ R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2
+ ) → (
+ ∀I,L1,L2,V,T,d.
+ L1 ⋕[V, d]L2 → L1 ⋕[T, d] L2 →
+ R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2
+ ) →
+ ∀d,T,L1,L2. L1 ⋕[T, d] L2 → R d T L1 L2.
+#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim (lleq_lleqa … H) -H
+/3 width=9 by lleqa_inv_lleq/
+qed-.