module Data.Type.List.Proof.Append where
import Data.Type.List.List
import Data.Type.Equality ((:=:)(..))
data Append ctx1 ctx2 ctx where
Append_Base :: Append ctx Nil ctx
Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)
trans ::
Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctx
trans app Append_Base = app
trans app (Append_Step app') = Append_Step (trans app app')
appendPf :: Append ctx1 ctx2 ctx -> (ctx :=: ctx1 :++: ctx2)
appendPf Append_Base = Refl
appendPf (Append_Step app) = case appendPf app of Refl -> Refl
length :: Append ctx1 ctx2 ctx3 -> Int
length Append_Base = 0
length (Append_Step app) = 1 + Data.Type.List.Proof.Append.length app