freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / theory.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
index 81422d2041dd0e9ba3184f4cc495cebf69aad800..6aa2e35b025dac8efd9284926ff34a0a386ced42 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma
@@ -208,7 +208,8 @@ nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → F
 nqed.
 
 nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
- #T; #l; nelim l;
+ #T; #l;
+ nelim l;
  nnormalize;
  ##[ ##1: napply (refl_eq ??)
  ##| ##2: #x; #y; #H;
@@ -239,4 +240,4 @@ nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a
  nrewrite > (associative_list T l [a] l1);
  nnormalize;
  napply (refl_eq ??).
-nqed.
\ No newline at end of file
+nqed.