gistfile1.idr

import Data.List

infixr 1 =~
infixr 1 >~
infixr 1 =~<

(=~) : (a:k) -> {b:k} -> (a = b) -> (a = b)
(=~) _ prf = prf

qed : {a:k} -> (a = a)
qed = Refl

(=~<) : (a:k) -> {b:k} -> (a = b) -> (a = b)
(=~<) _ prf = prf

(>~) : {a:k} -> {b:k} -> {c:k} -> (a = b) -> (b = c) -> (a = c)
(>~) x y = trans x y

length_append : (l:List a) -> (r:List a) -> length (l ++ r) = (length l + length r)
length_append [] r = 
  length ([] ++ r)
  =~
  0 + length r
  =~
  qed
length_append (x :: xs) r = 
  length (x :: xs ++ r)
  =~
  S (length (xs ++ r))
  =~< cong S (length_append xs r) >~
  S (length xs + length r)
  =~
  qed