module stlc.catComb.properities.propB where

open import stlc.catComb.properities.common
open import stlc.catComb.properities.propA

propB : ∀ {A} → (s : CatCombValue A) → ⊩ s
propB ⟨⟩ = unit
propB (`nat _) = nat
propB (s₁ , s₂) = pair ⦅ propB s₁ , propB s₂ ⦆
propB (cur f s) = cur λ { s₁ → propA f (pair ⦅ propB s , (_⇔_.from ⊩⇔⊩' s₁) ⦆) }
--- COPRODUCT ---
propB (L s) = inl (propB s)
propB (R s) = inr (propB s)
--- LIST OBJECT ---
propB [] = nil
propB (h ⦂ t) = cons (propB h) (propB t)