Proof about Kleene star idempotence in Agda.

Test.agda

open import Data.List as List
open import Data.List.Properties
open List-solver renaming (nil to :[] ; _⊕_ to _:++_; _⊜_ to _:==_)
open import Data.Product renaming (_×_ to _*_)

open import Relation.Binary
open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)
open import Relation.Nullary renaming (¬_ to not)

module Test {Token : Set}(eqTokenDec : Decidable {A = Token} _==_)  where

  infixr 5 _+_
  infixr 6 _o_
  infixl 7 _*

  data RegExp : Set where
    Emp : RegExp
    Eps : RegExp
    #_  : (a : Token) -> RegExp
    _o_ : (e e' : RegExp) -> RegExp
    _+_ : (e e' : RegExp) -> RegExp
    _*  : (e : RegExp) -> RegExp

  -- regular expression membership

  infix 3 _<-[[_]]
  infixr 6 _*_<=_
  infixr 6 _<+_ _+>_

  data _<-[[_]] : List Token -> RegExp -> Set where
    Eps    : List.[] <-[[ Eps ]]                       -- epsilon: empty string
    #_     : (a : Token) -> List.[ a ] <-[[ # a ]]     -- single token
    _*_<=_ : {xs ys zs : List Token}{e e' : RegExp}    -- concatenation of two REs
             (pr : xs <-[[ e ]])(pr' : ys <-[[ e' ]])
             (eq : zs == xs ++ ys) -> zs <-[[ e o e' ]]
    _<+_   : {xs : List Token}{e : RegExp}(e' : RegExp)  -- choice left
             -> (pr : xs <-[[ e ]]) -> xs <-[[ e + e' ]]           
    _+>_   : {xs : List Token}{e' : RegExp}(e : RegExp)   -- choice right
             -> (pr : xs <-[[ e' ]]) -> xs <-[[ e + e' ]]
    _*     : {xs : List Token}{e : RegExp} ->             -- Kleene star
             xs <-[[ Eps + e o e * ]]      ->
             xs <-[[ e * ]]


  -- regular expression equivalence

  infix 4 _:=:_

  _:=:_ : forall (e e' : RegExp) -> Set
  e :=: e' = forall (xs : List Token) -> (((pr : xs <-[[ e ]]) -> (xs <-[[ e' ]])) *
                                          ((pr : xs <-[[ e' ]]) -> (xs <-[[ e ]])))

  subsetLemma : forall {xs} e -> xs <-[[ e ]] -> xs <-[[ e * ]]
  subsetLemma {xs = xs} e pr = (_ +> pr * ((_ <+ Eps) *) <= solve 1 (\ xs -> xs :== xs :++ :[]) refl xs) *

  lemmaKleeneIdem : (e : RegExp) -> e * :=: (e *) *
  lemmaKleeneIdem e xs = subsetLemma (e *) , ?