Problem on refining data types indices

gistfile1.agda

open import Data.List
open import Data.Fin hiding (_+_)
open import Data.Nat renaming (ℕ to Nat)
open import Data.Product
open import Data.Vec using (Vec ; lookup)
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_ ; sym to symm)

module Test (A : Set)(fail : A) where

  data Foo : Nat -> Set where
    emp : forall {n} -> Foo n
    sym : forall {n} -> A -> Foo n
    var : forall {n} -> Fin (suc n) -> Foo n
    _o_ : forall {n} -> Foo n -> Foo n -> Foo n

  Con : Nat -> Set
  Con n = Vec (Foo n) (suc n)

  infix 1 _::_=>_

  data _::_=>_ {n} (G : Con n) : (Foo n × List A) -> (Nat × List A) -> Set where
     empty : forall x -> G :: (emp , x) => (1 , x)
     sym-success : forall a x -> G :: (sym a , (a ∷ x)) => (1 , a ∷ [])
     sym-failure : forall a b x -> ¬ (a == b) -> G :: (sym a , (b ∷ x)) => (1 , fail ∷ [])
     var : forall {x m o} {v : Fin (suc n)} -> G :: ((lookup v G) , x) => (m , o) -> G :: (var v , x) => (suc m , o)
     o-success : forall {e e' x x' y n n'} -> G :: (e , x ++ x' ++ y) => (n , x) -> G :: (e' , x' ++ y) => (n' , x') -> G :: (_o_ e e' , x ++ x' ++ y) => (suc (n + n') , x ++ x')
     o-fail1 : forall {e e' x x' y n o} -> G :: (e , x ++ x' ++ y) => (n , fail ∷ o) -> G :: (_o_ e e' , x ++ x' ++ y) => (suc n , fail ∷ [])
     o-fail2 : forall {e e' x x' y n n' o} -> G :: (e , x ++ x' ++ y) => (n , x) -> G :: (e' , x' ++ y) => (n' , fail ∷ o) -> G :: (_o_ e e' , x ++ x' ++ y) => (suc (n + n') , fail ∷ [])

  lemma : forall {n m m'}(G : Con n)(f : Foo n)(x : List A)(p p' : List A) -> G :: (f , x) => (m , p) -> G :: (f , x) => (m' , p') -> m == m' × p == p'
  lemma G .emp p .p .p (empty .p) (empty .p) = refl , refl
  lemma G .(sym a) .(a ∷ x) .(a ∷ []) .(a ∷ []) (sym-success a x) (sym-success .a .x) = refl , refl
  lemma G .(sym a) .(a ∷ x) .(a ∷ []) ._ (sym-success a x) (sym-failure .a .a .x x₁) = ⊥-elim (x₁ refl)
  lemma G .(sym a) .(a ∷ x) ._ .(a ∷ []) (sym-failure a .a x x₁) (sym-success .a .x) = ⊥-elim (x₁ refl)
  lemma G .(sym a) .(b ∷ x) ._ ._ (sym-failure a b x x₁) (sym-failure .a .b .x x₂) = refl , refl
  lemma G ._ x p p' (var pr) (var pr') = Data.Product.map (cong suc) (\ x -> x) (lemma _ _ _ _ _ pr pr')
  lemma G ._ ._ ._ p' (o-success pr pr₁) pr' = {!!}
  lemma G ._ ._ ._ p' (o-fail1 pr) pr' = {!pr'!}
  lemma G ._ ._ ._ p' (o-fail2 pr pr₁) pr' = {!!}