From c878697de62f713803d42e404918e57b6db92343 Mon Sep 17 00:00:00 2001
From: Kjetil Orbekk <kjetil.orbekk@gmail.com>
Date: Tue, 14 Feb 2017 16:13:54 -0500
Subject: Add list proof.

---
 Ch10.idr | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Ch10.idr b/Ch10.idr
index 9ab70ce..075aba4 100644
--- a/Ch10.idr
+++ b/Ch10.idr
@@ -21,5 +21,11 @@ mySplitIsTakeDrop (S k) [] = Refl
 mySplitIsTakeDrop (S k) (x::xs) =
   let rec = mySplitIsTakeDrop k xs in
   rewrite rec in Refl
+  
+takeDropIsIdentity : (n : Nat) -> (input : List a) -> take n input ++ drop n input = input
+takeDropIsIdentity Z input = Refl
+takeDropIsIdentity (S k) [] = Refl
+takeDropIsIdentity (S k) (x :: xs) =
+  rewrite takeDropIsIdentity k xs in Refl
 
 takeN : (n : Nat) -> (input : List a) -> TakeN input
-- 
cgit v1.2.3