-include "utility/utility.ma".
+(*include "utility/utility.ma".
-(*
nlemma fold_right_neList2_aux3 :
\forall T. \forall h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
#T; #h; #h'; #t; #t';
nchange in H2:(%) with ((S (len_neList T (a§§l1))) = (S (len_neList T (a§§l))));
*)
-include "freescale/byte8_lemmas.ma".
+(*include "freescale/byte8_lemmas.ma".
-(*
nlemma associative_plusb8_aux
: \forall e1,e2,e3,e4.
match plus_ex_d_dc e2 e4 with
(*...*)
*)
-include "compiler/ast_type_lemmas.ma".
+(*include "compiler/ast_type_lemmas.ma".
-(*
nlemma symmetric_eqasttype_aux1
: ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false.
#x1; #x2; #y2; ncases y2; nnormalize;