CIC has no eta-reduction/expansion

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
index bc7e6f9ceaeb06ced915251f53fc2204695e6d0e..eb4b32ce3eab9bdc42052b680d9101c557c8ba79 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma
@@ -346,12 +346,19 @@ ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1
   | xF ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))
   ].
 
-ndefinition b8_to_recb8 : Πb.rec_byte8 b.
- #b;
- nletin K ≝ (b8_to_recb8_aux3 (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
- nelim b in K:(%) ⊢ %;
- #e1; #e2; nnormalize; #H; napply H.
+(*
+nlemma b8_to_recb8 : Πb.rec_byte8 b.
+ #b; nletin K ≝ (b8_to_recb8_aux3 
+     (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
+ ncases b in K; #e1; #e2; #K; napply K;
 nqed.
+*)
+
+ndefinition b8_to_recb8 : Πb.rec_byte8 b ≝
+ λb.match b with
+     [ mk_byte8 h l ⇒ 
+       b8_to_recb8_aux3 
+        h l (b8_to_recb8_aux2 h (ex_to_recex h)) ].
 
 (* ottali → esadecimali *)
 ndefinition b8_of_bit ≝