-ndefinition locate_inv_ind ≝
-λx1,x2:Q.λP:Q → Q → Prop.
- λH1: ∀l',u'.x1≤l' → u'≤((2 * x1 + x2) / 3) → locate l' u' → P x1 x2.
- λH2: ∀l',u'. ((x1 + 2 * x2) / 3)≤l' → u'≤ x2 → locate l' u' → P x1 x2.
- λHterm:locate x1 x2.
- (λHcut:x1=x1 → x2=x2 → P x1 x2. Hcut (refl Q x1) (refl Q x2))
- match Hterm return λy1,y2.λp:locate y1 y2.
- x1=y1 → x2=y2 →P x1 x2
- with
- [ L l l' u' u Hle1 Hle2 r ⇒ ?(*H1 l l' u' u ?*)
- | H l l' u' u Hle1 Hle2 r ⇒ ?(*H2 l l' u' u ?*)].
-#a; #b; ##[ napply (H2 … r …) ##| napply (H1 … r …) ##] //.
+ndefinition locate_inv_ind':
+ ∀x1,x2:Q.∀P:Q → Q → Prop.
+ ∀H1: ∀l',u'.x1≤l' → u'≤((2 * x1 + x2) / 3) → locate l' u' → P x1 x2.
+ ∀H2: ∀l',u'. ((x1 + 2 * x2) / 3)≤l' → u'≤ x2 → locate l' u' → P x1 x2.
+ locate x1 x2 → P x1 x2.
+ #x1; #x2; #P; #H1; #H2; #p; ninversion p; #l; #l'; #u'; #u; #Ha; #Hb; #E1;
+ #E2; #E3; ndestruct; /2/ width=5.