[agda] finish value transitivity well-formedness lemma

code/gcbpv.agda

@@ -8,15 +8,9 @@ open import Data.Nat
 open import Data.Fin
 open import Data.Vec
 import Data.Vec
-import Data.Vec.Properties
+open import Data.Vec.Properties
 open ≡-Reasoning
 
-lookup-map : ∀ {a b n} {A : Set a} {B : Set b}
-             (i : Fin n) (f : A → B) (xs : Vec A n) →
-             lookup i (map f xs) ≡ f (lookup i xs)
-lookup-map zero    f (x ∷ xs) = refl
-lookup-map (suc i) f (x ∷ xs) = lookup-map i f xs
-
 data Stoup : Set where
   None : Stoup
   One  : Stoup
@@ -184,13 +178,25 @@ vty  (Γsq ⟪ i ⟫vsq) = (map (λ Vsq → Vsq ⟨ i ⟩vsq) (vty Γsq))
 vctxtrans : VCtxTC -> VCtx onevar
 vctxtrans Γsq = vctx (Vars Γsq) (map vtrans (vty Γsq))
 
+vtrans-dapp-lem : ∀ Vsq i ->  vtrans Vsq ⟨ i ⟩v ≡ Vsq ⟨ i ⟩vsq ⟨ i ⟩v
+vtrans-dapp-lem Vsq Top = refl
+vtrans-dapp-lem Vsq Bot = refl
+
 ctxttrans-dapp-lem : ∀ Γsq i -> vctxtrans Γsq ⟪ i ⟫v ≡ Γsq ⟪ i ⟫vsq ⟪ i ⟫v
 ctxttrans-dapp-lem Γsq i =
   begin
     vctxtrans Γsq ⟪ i ⟫v
-    ≡⟨ {!!} ⟩
-    vctxtrans Γsq ⟪ i ⟫v
-    ≡⟨ {!!} ⟩
+    ≡⟨ cong (vctx (Vars Γsq)) (
+      begin
+        map (λ A → A ⟨ i ⟩v) (vty (vctxtrans Γsq))
+        ≡⟨ sym (map-∘ (\A -> A ⟨ i ⟩v) vtrans (vty Γsq)) ⟩
+        map (λ Vsq → vtrans Vsq ⟨ i ⟩v) (vty Γsq)
+        ≡⟨ map-cong (λ x → vtrans-dapp-lem x i) (vty Γsq) ⟩
+        map (λ Vsq → Vsq ⟨ i ⟩vsq ⟨ i ⟩v) (vty Γsq)
+        ≡⟨ map-∘ ((λ A → A ⟨ i ⟩v)) ((λ Vsq → Vsq ⟨ i ⟩vsq)) (vty Γsq) ⟩
+        map (λ A → A ⟨ i ⟩v) (map (λ Vsq → Vsq ⟨ i ⟩vsq) (vty Γsq))
+      ∎
+    )⟩
     Γsq ⟪ i ⟫vsq ⟪ i ⟫v
   ∎