- L: ∀l,u. locate l ((2 * l + u) / 3) → locate l u
- | H: ∀l,u. locate ((l + 2 * u) / 3) u → locate l u.
+ L: ∀l,l',u',u. l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → locate l u
+ | H: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → locate l u.
+
+ndefinition locate_inv_ind ≝
+λx1,x2:Q.λP:Q → Q → Prop.
+ λH1: ∀l,l',u',u.l≤l' → u'≤((2 * l + u) / 3) → locate l' u' → P l u.
+ λH2: ∀l,l',u',u. ((l + 2 * u) / 3)≤l' → u'≤ u → locate l' u' → P l u.
+ λ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 y1 y2
+ 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; /2/; napply H2; //; (* Qui non va auto! *)
+
+ napply (H2 … r …); //;
+ /2/;
+ #h1; #h2; /2/; napply (H2 l l' u' u);