Issues with interface reduction of types in a mutual definition (Verified Applicative)

VerifiedApplciative.idr

------------------------------- Base Imports ---------------------------------
import Syntax.PreorderReasoning -- for long proofs
import Data.List -- for list lemmas
------------------------------ Custom Imports --------------------------------
import VerifiedFunctor

--------------------------------- Pragmas ------------------------------------
%default total
%hide Prelude.(<$>)
%hide Prelude.Interfaces.(<*>)
%hide Prelude.Interfaces.pure
%ambiguity_depth 15

------------------------------- Operators ------------------------------------
infixl 3 <*>

----------------------------- Definitions ------------------------------------

public export
interface VerifiedApplicative (f : Type -> Type) where
  -- functions
  pure : a -> f a
  (<*>) : f (a -> b) -> f a -> f b
  -- proofs
  idLaw : (x : f a) -> pure Prelude.Basics.id <*> x = x
  comLaw : {a, b : Type} 
        -> (x : f a) -> (g : f (a -> b)) -> (h : f (b -> c))
        -> (((pure (.)) <*> h) <*> g) <*> x = h <*> (g <*> x)
  homLaw : pure f <*> pure x = pure (f x)
  intLaw : {u : f (a -> b)} -> u <*> pure x = pure (\g => g x) <*> u

namespace ListLemmas
  public export    
  applyDistributesOverAppendRight : (VerifiedFunctor List, VerifiedApplicative List)                                   
                                 => (fs, gs : List (a -> b))    
                                 -> (xs : List a)                                                                                              
                                 -> (fs `Prelude.List.(++)` gs) <*> xs =    
                                      ((<*>) {f = List} fs xs) ++ (gs <*> xs)    
                                          
  public export    
  applyDistributesOverMap : (VerifiedApplicative List, VerifiedFunctor List)    
                         => (((<$>) {f = List} (g .) gs) <*> xs) = (g <$> (gs <*> xs))    
 
public export
implementation [vappl] VerifiedApplicative List where
  pure = (:: [])
  
  [] <*> xs = []
  (f :: fs) <*> xs = (f <$> xs) ++ (fs <*> xs)

  idLaw [] = Refl
  idLaw (x :: xs) = Calc $ -- hole : x :: ((id <$> xs) ++ []) = x :: xs
    |~ (x :: ((id <$> xs) ++ [])) -- The type of the LHS
    ~~ x :: xs ...(cong (\u => x :: u) (idLaw xs)) -- The type of RHS

  comLaw gs hs [] = Refl
  comLaw gs hs (x :: xs) = Calc $
   |~ (((x .) <$> hs) ++ ((((.) <$> xs) ++ []) <*> hs)) <*> gs
   ~~ (((x .) <$> hs) <*> gs) ++ (((((.) <$> xs) ++ []) <*> hs) <*> gs)
                ...( applyDistributesOverAppendRight ((x .) <$> hs) ((((.) <$> xs) ++ []) <*> hs) gs )
   ~~ ( (((x .) <$> hs) <*> gs) ++ (xs <*> (hs <*> gs)) ) 
                ...( cong (\u => (((x .) <$> hs) <*> gs) ++ u) (comLaw gs hs xs) )
   ~~ (x <$> (hs <*> gs)) ++ (xs <*> (hs <*> gs)) 
                ...( cong (\u => u ++ (xs <*> (hs <*> gs))) applyDistributesOverMap )

  homLaw = ?waiting5
  intLaw = ?waiting6

namespace ListLemmas
  --  applyDistributesOverAppendRight : VerifiedApplicative List 
  --                               => (fs, gs : List (a -> b)) 
  --                               -> (xs : List a)
  --                               -> (fs `Prelude.List.(++)` gs) <*> xs = 
  --                                    (fs <*> xs) ++ (gs <*> xs)
  applyDistributesOverAppendRight [] gs xs = ?thisDoesNotReduce
  applyDistributesOverAppendRight (f :: fs) gs xs = ?hole