\ /
V_______________________________________________________________ *)
-include "basics/list.ma".
-include "lambda/lambda_notation.ma".
+include "basics/lists/list.ma".
+include "pts_dummy/lambda_notation.ma".
inductive T : Type[0] ≝
| Sort: nat → T (* starts from 0 *)
].
lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
-#N #l elim l -l // #hd #tl #IHl #M >IHl //
+#N #l elim l -l // #hd #tl #IHl #M >IHl normalize //
qed.
(*