+
+(* Basic eliminators ********************************************************)
+
+lemma lex_ind (R) (Q:relation2 …):
+ Q (⋆) (⋆) →
+ (
+ ∀I,K1,K2. K1 ⪤[R] K2 → Q K1 K2 → Q (K1.ⓤ{I}) (K2.ⓤ{I})
+ ) → (
+ ∀I,K1,K2,V1,V2. K1 ⪤[R] K2 → Q K1 K2 → R K1 V1 V2 →Q (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ ) →
+ ∀L1,L2. L1 ⪤[R] L2 → Q L1 L2.
+#R #Q #IH1 #IH2 #IH3 #L1 #L2 * #f @pull_2 #H
+elim H -f -L1 -L2 // #f #I1 #I2 #K1 #K2 @pull_4 #H
+[ elim (isid_inv_next … H)
+| lapply (isid_inv_push … H ??)
+] -H [5:|*: // ] #Hf @pull_2 #H
+elim H -H /3 width=3 by ex2_intro/
+qed-.