+ bug fixed in the notation of exp
+ minor bugs fixed
(*** le *)
inductive nle (m:nat): predicate nat ≝
(*** le *)
inductive nle (m:nat): predicate nat ≝
| nle_succ_dx: ∀n. nle m n → nle m (↑n)
.
| nle_succ_dx: ∀n. nle m n → nle m (↑n)
.
(* GROUND NOTATION **********************************************************)
(* GROUND NOTATION **********************************************************)
-notation < "hvbox( f ^ break x )"
- left associative with precedence 65
+notation < "hvbox( term 66 f ^ break term 90 x )"
+ non associative with precedence 65
-notation > "hvbox( f ^ break x )"
- left associative with precedence 65
+notation > "hvbox( f ^ break term 90 x )"
+ non associative with precedence 65
-notation > "hvbox( f ^{ break term 46 X } break term 65 x )"
+notation > "hvbox( f ^{ break term 46 X } break term 90 x )"
non associative with precedence 65
for @{ 'Exp $X $f $x }.
non associative with precedence 65
for @{ 'Exp $X $f $x }.
#n #IH #f1 #g2 #H
elim (pr_eq_inv_push_sn … H) -H [|*: // ] #Hf10 *
elim (IH … Hf10) -IH -Hf10 #Hf12 #H1
#n #IH #f1 #g2 #H
elim (pr_eq_inv_push_sn … H) -H [|*: // ] #Hf10 *
elim (IH … Hf10) -IH -Hf10 #Hf12 #H1
+<pr_tls_succ /2 width=1 by conj/
qed-.
(*** eq_inv_pushs_dx *)
qed-.
(*** eq_inv_pushs_dx *)
#n #IH #f2 #g1 #H
elim (pr_eq_inv_push_dx … H) -H [|*: // ] #Hf02 *
elim (IH … Hf02) -IH -Hf02 #Hf12 #H2
#n #IH #f2 #g1 #H
elim (pr_eq_inv_push_dx … H) -H [|*: // ] #Hf02 *
elim (IH … Hf02) -IH -Hf02 #Hf12 #H2
+<pr_tls_succ /2 width=1 by conj/