Add list proof.

1 files changed, 6 insertions, 0 deletions

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