From 6ba2c98f5e7f9c00651d6050a98d1d7aab758958 Mon Sep 17 00:00:00 2001
From: gentzen
Date: Sun, 19 Jun 2011 06:55:22 0700
Subject: [PATCH] update baked in CoqPass.hs

build/CoqPass.hs  69 +++++++++++++++++++++
1 file changed, 27 insertions(+), 42 deletions()
diff git a/build/CoqPass.hs b/build/CoqPass.hs
index 5c0f49b..b81d20b 100644
 a/build/CoqPass.hs
+++ b/build/CoqPass.hs
@@ 15,6 +15,9 @@ import qualified Literal
import qualified Type
import qualified TypeRep
import qualified DataCon
+import qualified DsMonad
+import qualified IOEnv
+import qualified TcRnTypes
import qualified TyCon
import qualified Coercion
import qualified Var
@@ 33,7 +36,9 @@ import qualified Data.Typeable
import Data.Bits ((.&.), shiftL, (..))
import Prelude ( (++), (+), (==), Show, show, (.), ($) )
import qualified Prelude
+import qualified HscTypes
import qualified GHC.Base
+import qualified CoreMonad
import qualified System.IO.Unsafe
getTyConTyVars :: TyCon.TyCon > [Var.TyVar]
@@ 6300,8 +6305,8 @@ tree_of_nothing' unitTy prodTy gaTy __U0393_0 ec t =
T_Branch l r > (trace "X" (T_Branch (trace "X" ((trace "X" ((mapOptionTree0 (trace "X" (f)) (trace "X" (l))))))) (trace "X" ((trace "X" ((mapOptionTree0 (trace "X" (f)) (trace "X" (r)))))))))}))}
in mapOptionTree0 (trace "X" ((trace "X" ((flatten_leveled_type (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (__U0393_0))))))) (trace "X" ((trace "X" ((drop_lev (trace "X" (__U0393_0)) (trace "X" (((:) (trace "X" (ec)) (trace "X" (([])))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\t' > (trace "X" (MkLeveledHaskType (trace "X" (t')) (trace "X" (((:) (trace "X" (ec)) (trace "X" (([]))))))))))) (trace "X" (t1))))))))))))))))) (trace "X" (iHt2))))))))))))) (trace "X" (t))))))
flatten_skolemized_proof :: WeakExprVar0 > WeakExprVar0 > WeakExprVar0 > (() > (RawHaskType ()) > RawHaskType ()) > (() > (RawHaskType ()) > (RawHaskType ()) > (RawHaskType ()) > RawHaskType ()) > (() > (RawHaskType ()) > (RawHaskType ()) > (RawHaskType ()) > RawHaskType ()) > Garrow > (Tree (Prelude.Maybe Judg)) > (Tree (Prelude.Maybe Judg)) > (ND Judg SRule) > ND Judg Rule
flatten_skolemized_proof hetmet_flatten hetmet_unflatten hetmet_id unitTy prodTy gaTy gar h c x =
+flatten_skolemized_proof :: (() > (RawHaskType ()) > RawHaskType ()) > (() > (RawHaskType ()) > (RawHaskType ()) > (RawHaskType ()) > RawHaskType ()) > (() > (RawHaskType ()) > (RawHaskType ()) > (RawHaskType ()) > RawHaskType ()) > Garrow > (Tree (Prelude.Maybe Judg)) > (Tree (Prelude.Maybe Judg)) > (ND Judg SRule) > ND Judg Rule
+flatten_skolemized_proof unitTy prodTy gaTy gar h c x =
(trace "X" ((trace "X" (nd_map' (trace "X" ((trace "X" ((flatten_judgment (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy))))))) (trace "X" ((\h0 c0 x0 >
(trace "X" (case (trace "X" (x0)) of {
SFlat h1 c1 r >
@@ 6323,15 +6328,7 @@ flatten_skolemized_proof hetmet_flatten hetmet_unflatten hetmet_id unitTy prodTy
(:) h2 lev0 > (trace "X" ((trace "X" (eq_rect_r (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((trace "X" ((eq_rect_r (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkLeveledHaskType (trace "X" (__U03c3_)) (trace "X" (((:) (trace "X" (h2)) (trace "X" (lev0)))))))))))))) (trace "X" ((trace "X" ((ga_id (trace "X" ((Prelude.error "Proj Args"))) (trace "X" ((Prelude.error "Proj Args"))) (trace "X" ((Prelude.error "Proj Args"))) (trace "X" (gar)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((\_ > (trace "X" ((trace "X" (v2t (trace "X" (__U0393_0)) (trace "X" (h2))))))))) (trace "X" (([]))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((\_ > (trace "X" ((trace "X" (flatten_type (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (__U0393_0)) (trace "X" (KindStar)) (trace "X" (__U03c3_)))))))))))))))))))) (trace "X" ((trace "X" ((take_lev (trace "X" (__U0393_0)) (trace "X" (((:) (trace "X" (h2)) (trace "X" (lev0))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkLeveledHaskType (trace "X" (__U03c3_)) (trace "X" (((:) (trace "X" (h2)) (trace "X" (lev0)))))))))))))))))))))))) (trace "X" ((trace "X" ((drop_lev (trace "X" (__U0393_0)) (trace "X" (((:) (trace "X" (h2)) (trace "X" (lev0))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkLeveledHaskType (trace "X" (__U03c3_)) (trace "X" (((:) (trace "X" (h2)) (trace "X" (lev0)))))))))))))))))))))))}));
RGlobal __U0393_0 __U0394_0 __U03c3_ l wev >
(trace "X" (case (trace "X" (__U03c3_)) of {
 ([]) >
 (trace "X" (let {s = (trace "X" ((trace "X" (eqd_dec (trace "X" (coreVarEqDecidable)) (trace "X" ((trace "X" ((weakVarToCoreVar (trace "X" ((WExprVar (trace "X" ((trace "X" ((glob_wv (trace "X" ((Prelude.error "Proj Args"))) (trace "X" (l))))))))))))))) (trace "X" ((trace "X" ((weakVarToCoreVar (trace "X" ((WExprVar (trace "X" (hetmet_flatten))))))))))))))} in
 (trace "X" (case (trace "X" (s)) of {
 Prelude.True > (trace "X" (let {t = (trace "X" (\_ > (trace "X" ((trace "X" (flatten_type (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (__U0393_0)) (trace "X" (KindStar)) (trace "X" ((\_ > (trace "X" ((trace "X" (glob_tf (trace "X" (__U0393_0)) (trace "X" (l)) (trace "X" (wev)))))))))))))))} in (trace "X" (let {q = (trace "X" (\x1 > (trace "X" (RGlobal (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (([]))) (trace "X" ((trace "X" ((mkGlobal (trace "X" (__U0393_0)) (trace "X" (t)) (trace "X" (hetmet_id))))))) (trace "X" (x1))))))} in (trace "X" (Nd_rule (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (t)))))))) (trace "X" (([])))))))))))) (trace "X" ((trace "X" ((q (trace "X" (INil)))))))))))));
 Prelude.False >
 (trace "X" (let {s0 = (trace "X" ((trace "X" (eqd_dec (trace "X" (coreVarEqDecidable)) (trace "X" ((trace "X" ((weakVarToCoreVar (trace "X" ((WExprVar (trace "X" ((trace "X" ((glob_wv (trace "X" ((Prelude.error "Proj Args"))) (trace "X" (l))))))))))))))) (trace "X" ((trace "X" ((weakVarToCoreVar (trace "X" ((WExprVar (trace "X" (hetmet_unflatten))))))))))))))} in
 (trace "X" (case (trace "X" (s0)) of {
 Prelude.True > (trace "X" (let {t = (trace "X" (\_ > (trace "X" ((trace "X" (flatten_type (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (__U0393_0)) (trace "X" (KindStar)) (trace "X" ((\_ > (trace "X" ((trace "X" (glob_tf (trace "X" (__U0393_0)) (trace "X" (l)) (trace "X" (wev)))))))))))))))} in (trace "X" (let {q = (trace "X" (\x1 > (trace "X" (RGlobal (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (([]))) (trace "X" ((trace "X" ((mkGlobal (trace "X" (__U0393_0)) (trace "X" (t)) (trace "X" (hetmet_id))))))) (trace "X" (x1))))))} in (trace "X" (Nd_rule (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (t)))))))) (trace "X" (([])))))))))))) (trace "X" ((trace "X" ((q (trace "X" (INil)))))))))))));
 Prelude.False > (trace "X" (Nd_rule (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((\_ > (trace "X" ((trace "X" (flatten_type (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (__U0393_0)) (trace "X" (KindStar)) (trace "X" ((\_ > (trace "X" ((trace "X" (glob_tf (trace "X" (__U0393_0)) (trace "X" (l)) (trace "X" (wev)))))))))))))))))))))) (trace "X" (([])))))))))))) (trace "X" ((trace "X" ((eq_rect_r (trace "X" ((\_ > (trace "X" ((trace "X" (glob_tf (trace "X" (__U0393_0)) (trace "X" (l)) (trace "X" (wev))))))))) (trace "X" ((RGlobal (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (([]))) (trace "X" (l)) (trace "X" (wev))))) (trace "X" ((\_ > (trace "X" ((trace "X" (flatten_type (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (__U0393_0)) (trace "X" (KindStar)) (trace "X" ((\_ > (trace "X" ((trace "X" (glob_tf (trace "X" (__U0393_0)) (trace "X" (l)) (trace "X" (wev)))))))))))))))))))))))}))))}))));
+ ([]) > (trace "X" (Nd_rule (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((\_ > (trace "X" ((trace "X" (flatten_type (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (__U0393_0)) (trace "X" (KindStar)) (trace "X" ((\_ > (trace "X" ((trace "X" (glob_tf (trace "X" (__U0393_0)) (trace "X" (l)) (trace "X" (wev)))))))))))))))))))))) (trace "X" (([])))))))))))) (trace "X" ((trace "X" ((eq_rect_r (trace "X" ((\_ > (trace "X" ((trace "X" (glob_tf (trace "X" (__U0393_0)) (trace "X" (l)) (trace "X" (wev))))))))) (trace "X" ((RGlobal (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (([]))) (trace "X" (l)) (trace "X" (wev))))) (trace "X" ((\_ > (trace "X" ((trace "X" (flatten_type (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (__U0393_0)) (trace "X" (KindStar)) (trace "X" ((\_ > (trace "X" ((trace "X" (glob_tf (trace "X" (__U0393_0)) (trace "X" (l)) (trace "X" (wev)))))))))))))))))))))));
(:) ec lev > (trace "X" ((trace "X" (Prelude.error (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('R')) (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('>')) (trace "X" (((:) (trace "X" ('0')) (trace "X" (((:) (trace "X" (';')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('k')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
RLam __U0393_0 __U0394_0 __U03a3_ tx te lev >
(trace "X" (case (trace "X" (lev)) of {
@@ 6405,9 +6402,9 @@ flatten_proof :: (Tree (Prelude.Maybe Judg)) > (Tree (Prelude.Maybe Judg)) > (
flatten_proof =
(trace "X" ((trace "X" (Prelude.error (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" (',')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('k')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('z')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('\'')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
skolemize_and_flatten_proof :: WeakExprVar0 > WeakExprVar0 > WeakExprVar0 > (() > (RawHaskType ()) > RawHaskType ()) > (() > (RawHaskType ()) > (RawHaskType ()) > (RawHaskType ()) > RawHaskType ()) > (() > (RawHaskType ()) > (RawHaskType ()) > (RawHaskType ()) > RawHaskType ()) > Garrow > (Tree (Prelude.Maybe Judg)) > (Tree (Prelude.Maybe Judg)) > (ND Judg Rule) > ND Judg Rule
skolemize_and_flatten_proof hetmet_flatten hetmet_unflatten hetmet_id unitTy prodTy gaTy gar h c x =
 (trace "X" ((trace "X" (eq_rect_r (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((trace "X" ((flatten_judgment (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (skolemize_judgment)) (trace "X" (h)))))))))))) (trace "X" ((trace "X" ((eq_rect_r (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((trace "X" ((flatten_judgment (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (skolemize_judgment)) (trace "X" (c)))))))))))) (trace "X" ((trace "X" ((flatten_skolemized_proof (trace "X" (hetmet_flatten)) (trace "X" (hetmet_unflatten)) (trace "X" (hetmet_id)) (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (gar)) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (skolemize_judgment)) (trace "X" (h))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (skolemize_judgment)) (trace "X" (c))))))) (trace "X" ((trace "X" ((skolemize_proof (trace "X" (h)) (trace "X" (c)) (trace "X" (x)))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\x0 > (trace "X" ((trace "X" (flatten_judgment (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" ((trace "X" ((skolemize_judgment (trace "X" (x0)))))))))))))) (trace "X" (c)))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\x0 > (trace "X" ((trace "X" (flatten_judgment (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" ((trace "X" ((skolemize_judgment (trace "X" (x0)))))))))))))) (trace "X" (h)))))))))))
+skolemize_and_flatten_proof :: (() > (RawHaskType ()) > RawHaskType ()) > (() > (RawHaskType ()) > (RawHaskType ()) > (RawHaskType ()) > RawHaskType ()) > (() > (RawHaskType ()) > (RawHaskType ()) > (RawHaskType ()) > RawHaskType ()) > Garrow > (Tree (Prelude.Maybe Judg)) > (Tree (Prelude.Maybe Judg)) > (ND Judg Rule) > ND Judg Rule
+skolemize_and_flatten_proof unitTy prodTy gaTy gar h c x =
+ (trace "X" ((trace "X" (eq_rect_r (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((trace "X" ((flatten_judgment (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (skolemize_judgment)) (trace "X" (h)))))))))))) (trace "X" ((trace "X" ((eq_rect_r (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((trace "X" ((flatten_judgment (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (skolemize_judgment)) (trace "X" (c)))))))))))) (trace "X" ((trace "X" ((flatten_skolemized_proof (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" (gar)) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (skolemize_judgment)) (trace "X" (h))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (skolemize_judgment)) (trace "X" (c))))))) (trace "X" ((trace "X" ((skolemize_proof (trace "X" (h)) (trace "X" (c)) (trace "X" (x)))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\x0 > (trace "X" ((trace "X" (flatten_judgment (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" ((trace "X" ((skolemize_judgment (trace "X" (x0)))))))))))))) (trace "X" (c)))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\x0 > (trace "X" ((trace "X" (flatten_judgment (trace "X" (unitTy)) (trace "X" (prodTy)) (trace "X" (gaTy)) (trace "X" ((trace "X" ((skolemize_judgment (trace "X" (x0)))))))))))))) (trace "X" (h)))))))))))
__U0393_ :: TypeEnv
__U0393_ =
@@ 6614,20 +6611,8 @@ hetmet_esc' :: Var.Var > WeakExprVar0
hetmet_esc' hetmet_esc =
(trace "X" ((trace "X" (coreVarToWeakExprVarOrError (trace "X" (hetmet_esc))))))
hetmet_flatten' :: Var.Var > WeakExprVar0
hetmet_flatten' hetmet_flatten =
 (trace "X" ((trace "X" (coreVarToWeakExprVarOrError (trace "X" (hetmet_flatten))))))

hetmet_unflatten' :: Var.Var > WeakExprVar0
hetmet_unflatten' hetmet_unflatten =
 (trace "X" ((trace "X" (coreVarToWeakExprVarOrError (trace "X" (hetmet_unflatten))))))

hetmet_flattened_id' :: Var.Var > WeakExprVar0
hetmet_flattened_id' hetmet_flattened_id =
 (trace "X" ((trace "X" (coreVarToWeakExprVarOrError (trace "X" (hetmet_flattened_id))))))

coreToCoreExpr' :: Prelude.Bool > Prelude.Bool > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > UniqSupply.UniqSupply > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > (CoreSyn.Expr Var.Var) > OrError (CoreSyn.Expr Var.Var)
coreToCoreExpr' do_flatten do_skolemize hetmet_brak hetmet_esc hetmet_flatten hetmet_unflatten hetmet_flattened_id uniqueSupply hetmet_PGArrowTyCon hetmet_PGArrow_unit_TyCon hetmet_PGArrow_tensor_TyCon hetmet_pga_id hetmet_pga_comp hetmet_pga_first hetmet_pga_second hetmet_pga_cancell hetmet_pga_cancelr hetmet_pga_uncancell hetmet_pga_uncancelr hetmet_pga_assoc hetmet_pga_unassoc hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr cex =
+coreToCoreExpr' :: Prelude.Bool > Prelude.Bool > Var.Var > Var.Var > UniqSupply.UniqSupply > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > (CoreSyn.Expr Var.Var) > OrError (CoreSyn.Expr Var.Var)
+coreToCoreExpr' do_flatten do_skolemize hetmet_brak hetmet_esc uniqueSupply hetmet_PGArrowTyCon hetmet_PGArrow_unit_TyCon hetmet_PGArrow_tensor_TyCon hetmet_pga_id hetmet_pga_comp hetmet_pga_first hetmet_pga_second hetmet_pga_cancell hetmet_pga_cancelr hetmet_pga_uncancell hetmet_pga_uncancelr hetmet_pga_assoc hetmet_pga_unassoc hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr cex =
(trace "X" ((trace "X" (addErrorMessage (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('S')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (':')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreExprToString)) (trace "X" (cex))))))))))))
(trace "X" ((trace "X" ((addErrorMessage (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (':')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreTypeToString)) (trace "X" ((trace "X" ((CoreUtils.exprType (trace "X" (cex)))))))))))))))))
(trace "X" ((trace "X" ((orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (cex))))))) (trace "X" ((\we >
@@ 6639,30 +6624,30 @@ coreToCoreExpr' do_flatten do_skolemize hetmet_brak hetmet_esc hetmet_flatten he
(trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((weakExprToStrongExpr (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03c6_)) (trace "X" (__U03c8_)) (trace "X" (__U03be_)) (trace "X" ((\x > (trace "X" (Prelude.True))))) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (we))))))) (trace "X" ((\e >
(trace "X" ((trace "X" (addErrorMessage (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('k')) (trace "X" (((:) (trace "X" ('S')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('.')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))
(trace "X" ((case (trace "X" (do_skolemize)) of {
 Prelude.True > (trace "X" (let {haskProof = (trace "X" ((trace "X" (skolemize_and_flatten_proof (trace "X" ((trace "X" ((hetmet_flatten' (trace "X" (hetmet_flatten))))))) (trace "X" ((trace "X" ((hetmet_unflatten' (trace "X" (hetmet_unflatten))))))) (trace "X" ((trace "X" ((hetmet_flattened_id' (trace "X" (hetmet_flattened_id))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_unit (trace "X" (hetmet_PGArrow_unit_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_prod (trace "X" (hetmet_PGArrow_tensor_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_type (trace "X" (hetmet_PGArrowTyCon))))))))) (trace "X" ((trace "X" ((my_ga (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr))))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_)) (trace "X" ((trace "X" ((expr2antecedent (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e)))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03c4_)))))))) (trace "X" (([])))))))))))) (trace "X" ((trace "X" ((expr2proof (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e)))))))))))} in (trace "X" ((trace "X" (orErrorBind (trace "X" ((OK (trace "X" ((trace "X" ((unsafeCoerce (trace "X" (proof2expr)) (trace "X" (eqDecidableNat)) (trace "X" (freshNat)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" ((\_ > (trace "X" ((trace "X" (flatten_type (trace "X" ((\_ > (trace "X" ((trace "X" (ga_unit (trace "X" (hetmet_PGArrow_unit_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_prod (trace "X" (hetmet_PGArrow_tensor_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_type (trace "X" (hetmet_PGArrowTyCon))))))))) (trace "X" (__U0393_)) (trace "X" (KindStar)) (trace "X" (__U03c4_))))))))) (trace "X" (([]))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((trace "X" ((flatten_leveled_type (trace "X" ((\_ > (trace "X" ((trace "X" (ga_unit (trace "X" (hetmet_PGArrow_unit_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_prod (trace "X" (hetmet_PGArrow_tensor_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_type (trace "X" (hetmet_PGArrowTyCon))))))))) (trace "X" (__U0393_))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_)) (trace "X" ((trace "X" ((expr2antecedent (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e))))))))))))))))) (trace "X" ((\x > (trace "X" ((trace "X" (Prelude.error (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('q')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (natToStringInstance)) (trace "X" (haskProof)) (trace "X" (O)))))))))) (trace "X" ((\e' > (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((snd (trace "X" (e'))))))) (trace "X" ((\e'' > (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((strongExprToWeakExpr (trace "X" ((trace "X" ((hetmet_brak' (trace "X" (hetmet_brak))))))) (trace "X" ((trace "X" ((hetmet_esc' (trace "X" (hetmet_esc))))))) (trace "X" (mkWeakTypeVar0)) (trace "X" (mkWeakCoerVar0)) (trace "X" (mkWeakExprVar0)) (trace "X" (eqDecidableNat)) (trace "X" (natToStringInstance)) (trace "X" (uniqueSupply)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" ((trace "X" ((projT1 (trace "X" (e''))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (flatten_type (trace "X" ((\_ > (trace "X" ((trace "X" (ga_unit (trace "X" (hetmet_PGArrow_unit_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_prod (trace "X" (hetmet_PGArrow_tensor_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_type (trace "X" (hetmet_PGArrowTyCon))))))))) (trace "X" (__U0393_)) (trace "X" (KindStar)) (trace "X" (__U03c4_))))))))) (trace "X" (([]))) (trace "X" ((trace "X" ((projT2 (trace "X" (e''))))))) (trace "X" (INil))))))) (trace "X" ((\q > (trace "X" (OK (trace "X" ((trace "X" ((weakExprToCoreExpr (trace "X" (q))))))))))))))))))))))))))))))));
+ Prelude.True > (trace "X" (let {haskProof = (trace "X" ((trace "X" (skolemize_and_flatten_proof (trace "X" ((\_ > (trace "X" ((trace "X" (ga_unit (trace "X" (hetmet_PGArrow_unit_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_prod (trace "X" (hetmet_PGArrow_tensor_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_type (trace "X" (hetmet_PGArrowTyCon))))))))) (trace "X" ((trace "X" ((my_ga (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr))))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_)) (trace "X" ((trace "X" ((expr2antecedent (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e)))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03c4_)))))))) (trace "X" (([])))))))))))) (trace "X" ((trace "X" ((expr2proof (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e)))))))))))} in (trace "X" ((trace "X" (orErrorBind (trace "X" ((OK (trace "X" ((trace "X" ((unsafeCoerce (trace "X" (proof2expr)) (trace "X" (eqDecidableNat)) (trace "X" (freshNat)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" ((\_ > (trace "X" ((trace "X" (flatten_type (trace "X" ((\_ > (trace "X" ((trace "X" (ga_unit (trace "X" (hetmet_PGArrow_unit_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_prod (trace "X" (hetmet_PGArrow_tensor_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_type (trace "X" (hetmet_PGArrowTyCon))))))))) (trace "X" (__U0393_)) (trace "X" (KindStar)) (trace "X" (__U03c4_))))))))) (trace "X" (([]))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((trace "X" ((flatten_leveled_type (trace "X" ((\_ > (trace "X" ((trace "X" (ga_unit (trace "X" (hetmet_PGArrow_unit_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_prod (trace "X" (hetmet_PGArrow_tensor_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_type (trace "X" (hetmet_PGArrowTyCon))))))))) (trace "X" (__U0393_))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_)) (trace "X" ((trace "X" ((expr2antecedent (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e))))))))))))))))) (trace "X" ((\x > (trace "X" ((trace "X" (Prelude.error (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('q')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (natToStringInstance)) (trace "X" (haskProof)) (trace "X" (O)))))))))) (trace "X" ((\e' > (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((snd (trace "X" (e'))))))) (trace "X" ((\e'' > (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((strongExprToWeakExpr (trace "X" ((trace "X" ((hetmet_brak' (trace "X" (hetmet_brak))))))) (trace "X" ((trace "X" ((hetmet_esc' (trace "X" (hetmet_esc))))))) (trace "X" (mkWeakTypeVar0)) (trace "X" (mkWeakCoerVar0)) (trace "X" (mkWeakExprVar0)) (trace "X" (eqDecidableNat)) (trace "X" (natToStringInstance)) (trace "X" (uniqueSupply)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" ((trace "X" ((projT1 (trace "X" (e''))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (flatten_type (trace "X" ((\_ > (trace "X" ((trace "X" (ga_unit (trace "X" (hetmet_PGArrow_unit_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_prod (trace "X" (hetmet_PGArrow_tensor_TyCon))))))))) (trace "X" ((\_ > (trace "X" ((trace "X" (ga_type (trace "X" (hetmet_PGArrowTyCon))))))))) (trace "X" (__U0393_)) (trace "X" (KindStar)) (trace "X" (__U03c4_))))))))) (trace "X" (([]))) (trace "X" ((trace "X" ((projT2 (trace "X" (e''))))))) (trace "X" (INil))))))) (trace "X" ((\q > (trace "X" (OK (trace "X" ((trace "X" ((weakExprToCoreExpr (trace "X" (q))))))))))))))))))))))))))))))));
Prelude.False >
(trace "X" (case (trace "X" (do_flatten)) of {
Prelude.True > (trace "X" (let {haskProof = (trace "X" ((trace "X" (flatten_proof (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_)) (trace "X" ((trace "X" ((expr2antecedent (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e)))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03c4_)))))))) (trace "X" (([])))))))))))) (trace "X" ((trace "X" ((expr2proof (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e)))))))))))} in (trace "X" ((trace "X" (orErrorBind (trace "X" ((OK (trace "X" ((trace "X" ((unsafeCoerce (trace "X" (proof2expr)) (trace "X" (eqDecidableNat)) (trace "X" (freshNat)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_)) (trace "X" ((trace "X" ((expr2antecedent (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e)))))))))))) (trace "X" ((\x > (trace "X" ((trace "X" (Prelude.error (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('q')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (natToStringInstance)) (trace "X" (haskProof)) (trace "X" (O)))))))))) (trace "X" ((\e' > (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((snd (trace "X" (e'))))))) (trace "X" ((\e'' > (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((strongExprToWeakExpr (trace "X" ((trace "X" ((hetmet_brak' (trace "X" (hetmet_brak))))))) (trace "X" ((trace "X" ((hetmet_esc' (trace "X" (hetmet_esc))))))) (trace "X" (mkWeakTypeVar0)) (trace "X" (mkWeakCoerVar0)) (trace "X" (mkWeakExprVar0)) (trace "X" (eqDecidableNat)) (trace "X" (natToStringInstance)) (trace "X" (uniqueSupply)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" ((trace "X" ((projT1 (trace "X" (e''))))))) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" ((trace "X" ((projT2 (trace "X" (e''))))))) (trace "X" (INil))))))) (trace "X" ((\q > (trace "X" (OK (trace "X" ((trace "X" ((weakExprToCoreExpr (trace "X" (q))))))))))))))))))))))))))))))));
Prelude.False > (trace "X" (let {haskProof = (trace "X" ((trace "X" (expr2proof (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e))))))} in (trace "X" ((trace "X" (orErrorBind (trace "X" ((OK (trace "X" ((trace "X" ((unsafeCoerce (trace "X" (proof2expr)) (trace "X" (eqDecidableNat)) (trace "X" (freshNat)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_)) (trace "X" ((trace "X" ((expr2antecedent (trace "X" (coreVarEqDecidable)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" (__U03be_)) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" (e)))))))))))) (trace "X" ((\x > (trace "X" ((trace "X" (Prelude.error (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('q')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (natToStringInstance)) (trace "X" (haskProof)) (trace "X" (O)))))))))) (trace "X" ((\e' > (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((snd (trace "X" (e'))))))) (trace "X" ((\e'' > (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((strongExprToWeakExpr (trace "X" ((trace "X" ((hetmet_brak' (trace "X" (hetmet_brak))))))) (trace "X" ((trace "X" ((hetmet_esc' (trace "X" (hetmet_esc))))))) (trace "X" (mkWeakTypeVar0)) (trace "X" (mkWeakCoerVar0)) (trace "X" (mkWeakExprVar0)) (trace "X" (eqDecidableNat)) (trace "X" (natToStringInstance)) (trace "X" (uniqueSupply)) (trace "X" (__U0393_)) (trace "X" (__U0394_)) (trace "X" ((trace "X" ((projT1 (trace "X" (e''))))))) (trace "X" (__U03c4_)) (trace "X" (([]))) (trace "X" ((trace "X" ((projT2 (trace "X" (e''))))))) (trace "X" (INil))))))) (trace "X" ((\q > (trace "X" (OK (trace "X" ((trace "X" ((weakExprToCoreExpr (trace "X" (q))))))))))))))))))))))))))))))))}))}))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
coreToCoreExpr :: Prelude.Bool > Prelude.Bool > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > UniqSupply.UniqSupply > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > (CoreSyn.Expr Var.Var) > CoreSyn.Expr Var.Var
coreToCoreExpr do_flatten do_skolemize hetmet_brak hetmet_esc hetmet_flatten hetmet_unflatten hetmet_flattened_id uniqueSupply hetmet_PGArrowTyCon hetmet_PGArrow_unit_TyCon hetmet_PGArrow_tensor_TyCon hetmet_pga_id hetmet_pga_comp hetmet_pga_first hetmet_pga_second hetmet_pga_cancell hetmet_pga_cancelr hetmet_pga_uncancell hetmet_pga_uncancelr hetmet_pga_assoc hetmet_pga_unassoc hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr ce =
 (trace "X" (case (trace "X" ((trace "X" (coreToCoreExpr' (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (hetmet_flatten)) (trace "X" (hetmet_unflatten)) (trace "X" (hetmet_flattened_id)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr)) (trace "X" (ce)))))) of {
+coreToCoreExpr :: Prelude.Bool > Prelude.Bool > Var.Var > Var.Var > UniqSupply.UniqSupply > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > (CoreSyn.Expr Var.Var) > CoreSyn.Expr Var.Var
+coreToCoreExpr do_flatten do_skolemize hetmet_brak hetmet_esc uniqueSupply hetmet_PGArrowTyCon hetmet_PGArrow_unit_TyCon hetmet_PGArrow_tensor_TyCon hetmet_pga_id hetmet_pga_comp hetmet_pga_first hetmet_pga_second hetmet_pga_cancell hetmet_pga_cancelr hetmet_pga_uncancell hetmet_pga_uncancelr hetmet_pga_assoc hetmet_pga_unassoc hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr ce =
+ (trace "X" (case (trace "X" ((trace "X" (coreToCoreExpr' (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr)) (trace "X" (ce)))))) of {
Error s > (trace "X" ((trace "X" (Prelude.error (trace "X" (s))))));
OK x > (trace "X" (x))}))
coreToCoreBind :: Prelude.Bool > Prelude.Bool > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > UniqSupply.UniqSupply > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > (CoreSyn.Bind Var.Var) > CoreSyn.Bind Var.Var
coreToCoreBind do_flatten do_skolemize hetmet_brak hetmet_esc hetmet_flatten hetmet_unflatten hetmet_flattened_id uniqueSupply hetmet_PGArrowTyCon hetmet_PGArrow_unit_TyCon hetmet_PGArrow_tensor_TyCon hetmet_pga_id hetmet_pga_comp hetmet_pga_first hetmet_pga_second hetmet_pga_cancell hetmet_pga_cancelr hetmet_pga_uncancell hetmet_pga_uncancelr hetmet_pga_assoc hetmet_pga_unassoc hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr binds =
+coreToCoreBind :: Prelude.Bool > Prelude.Bool > Var.Var > Var.Var > UniqSupply.UniqSupply > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > (CoreSyn.Bind Var.Var) > CoreSyn.Bind Var.Var
+coreToCoreBind do_flatten do_skolemize hetmet_brak hetmet_esc uniqueSupply hetmet_PGArrowTyCon hetmet_PGArrow_unit_TyCon hetmet_PGArrow_tensor_TyCon hetmet_pga_id hetmet_pga_comp hetmet_pga_first hetmet_pga_second hetmet_pga_cancell hetmet_pga_cancelr hetmet_pga_uncancell hetmet_pga_uncancelr hetmet_pga_assoc hetmet_pga_unassoc hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr binds =
(trace "X" (case (trace "X" (binds)) of {
 CoreSyn.NonRec v e > (trace "X" (let {e' = (trace "X" ((trace "X" (coreToCoreExpr (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (hetmet_flatten)) (trace "X" (hetmet_unflatten)) (trace "X" (hetmet_flattened_id)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr)) (trace "X" (e))))))} in (trace "X" (CoreSyn.NonRec (trace "X" ((trace "X" ((Var.setVarType (trace "X" (v)) (trace "X" ((trace "X" ((CoreUtils.exprType (trace "X" (e')))))))))))) (trace "X" (e'))))));
+ CoreSyn.NonRec v e > (trace "X" (let {e' = (trace "X" ((trace "X" (coreToCoreExpr (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr)) (trace "X" (e))))))} in (trace "X" (CoreSyn.NonRec (trace "X" ((trace "X" ((Var.setVarType (trace "X" (v)) (trace "X" ((trace "X" ((CoreUtils.exprType (trace "X" (e')))))))))))) (trace "X" (e'))))));
CoreSyn.Rec lbe > (trace "X" (CoreSyn.Rec (trace "X" ((trace "X" ((map (trace "X" ((\ve > (trace "X" (case (trace "X" (ve)) of {
 (,) v e > (trace "X" ((,) (trace "X" (v)) (trace "X" ((trace "X" ((coreToCoreExpr (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (hetmet_flatten)) (trace "X" (hetmet_unflatten)) (trace "X" (hetmet_flattened_id)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr)) (trace "X" (e)))))))))}))))) (trace "X" (lbe)))))))))}))
+ (,) v e > (trace "X" ((,) (trace "X" (v)) (trace "X" ((trace "X" ((coreToCoreExpr (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr)) (trace "X" (e)))))))))}))))) (trace "X" (lbe)))))))))}))
coqPassCoreToCore' :: Prelude.Bool > Prelude.Bool > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > UniqSupply.UniqSupply > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > (([]) (CoreSyn.Bind Var.Var)) > ([]) (CoreSyn.Bind Var.Var)
coqPassCoreToCore' do_flatten do_skolemize hetmet_brak hetmet_esc hetmet_flatten hetmet_unflatten hetmet_flattened_id uniqueSupply hetmet_PGArrowTyCon hetmet_PGArrow_unit_TyCon hetmet_PGArrow_tensor_TyCon hetmet_pga_id hetmet_pga_comp hetmet_pga_first hetmet_pga_second hetmet_pga_cancell hetmet_pga_cancelr hetmet_pga_uncancell hetmet_pga_uncancelr hetmet_pga_assoc hetmet_pga_unassoc hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr lbinds =
 (trace "X" ((trace "X" (map (trace "X" ((trace "X" ((coreToCoreBind (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (hetmet_flatten)) (trace "X" (hetmet_unflatten)) (trace "X" (hetmet_flattened_id)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr))))))) (trace "X" (lbinds))))))
+coqPassCoreToCore' :: Prelude.Bool > Prelude.Bool > Var.Var > Var.Var > UniqSupply.UniqSupply > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > (([]) (CoreSyn.Bind Var.Var)) > ([]) (CoreSyn.Bind Var.Var)
+coqPassCoreToCore' do_flatten do_skolemize hetmet_brak hetmet_esc uniqueSupply hetmet_PGArrowTyCon hetmet_PGArrow_unit_TyCon hetmet_PGArrow_tensor_TyCon hetmet_pga_id hetmet_pga_comp hetmet_pga_first hetmet_pga_second hetmet_pga_cancell hetmet_pga_cancelr hetmet_pga_uncancell hetmet_pga_uncancelr hetmet_pga_assoc hetmet_pga_unassoc hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr lbinds =
+ (trace "X" ((trace "X" (map (trace "X" ((trace "X" ((coreToCoreBind (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr))))))) (trace "X" (lbinds))))))
coqPassCoreToCore :: Prelude.Bool > Prelude.Bool > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > UniqSupply.UniqSupply > (([]) (CoreSyn.Bind Var.Var)) > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > TyCon.TyCon > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > Var.Var > ([]) (CoreSyn.Bind Var.Var)
coqPassCoreToCore do_flatten do_skolemize hetmet_brak hetmet_esc hetmet_flatten hetmet_unflatten hetmet_flattened_id uniqueSupply lbinds hetmet_PGArrowTyCon hetmet_PGArrow_unit_TyCon hetmet_PGArrow_tensor_TyCon hetmet_PGArrow_exponent_TyCon hetmet_pga_id hetmet_pga_comp hetmet_pga_first hetmet_pga_second hetmet_pga_cancell hetmet_pga_cancelr hetmet_pga_uncancell hetmet_pga_uncancelr hetmet_pga_assoc hetmet_pga_unassoc hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap hetmet_pga_applyl hetmet_pga_applyr hetmet_pga_curryl hetmet_pga_curryr hetmet_pga_loopl hetmet_pga_loopr =
 (trace "X" ((trace "X" (coqPassCoreToCore' (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (hetmet_flatten)) (trace "X" (hetmet_unflatten)) (trace "X" (hetmet_flattened_id)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrowTyCon)) (trace "X" (hetmet_PGArrow_unit_TyCon)) (trace "X" (hetmet_PGArrow_tensor_TyCon)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr)) (trace "X" (lbinds))))))
+coqPassCoreToCore :: Prelude.Bool > Prelude.Bool > (Prelude.String > Prelude.String > CoreMonad.CoreM Var.Var) > (Prelude.String > Prelude.String > CoreMonad.CoreM TyCon.TyCon) > UniqSupply.UniqSupply > (([]) (CoreSyn.Bind Var.Var)) > CoreMonad.CoreM (([]) (CoreSyn.Bind Var.Var))
+coqPassCoreToCore do_flatten do_skolemize dsLookupVar dsLookupTyc uniqueSupply lbinds =
+ (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('s')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('k')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_brak > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('s')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('c')) (trace "X" ([]))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_esc > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupTyc (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('w')) (trace "X" ([])))))))))))))))))))))))))))) (trace "X" ((\hetmet_PGArrow > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupTyc (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('w')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" ('U')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('t')) (trace "X" ([]))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_PGArrow_unit > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupTyc (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('w')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_PGArrow_tensor > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupTyc (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('w')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_PGArrow_exponent > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('d')) (trace "X" ([]))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_id > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('p')) (trace "X" ([]))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_comp > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('t')) (trace "X" ([])))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_first > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" ([]))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_second > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('l')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_cancell > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('r')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_cancelr > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('l')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_uncancell > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('r')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_uncancelr > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('c')) (trace "X" ([])))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_assoc > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('c')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_unassoc > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('y')) (trace "X" ([]))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_copy > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('p')) (trace "X" ([]))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_drop > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('p')) (trace "X" ([]))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_swap > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('l')) (trace "X" ([]))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_applyl > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('r')) (trace "X" ([]))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_applyr > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('l')) (trace "X" ([]))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_curryl > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('r')) (trace "X" ([]))))))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_curryr > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('l')) (trace "X" ([])))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_loopl > (trace "X" ((trace "X" ((Prelude.>>=) (trace "X" ((trace "X" ((dsLookupVar (trace "X" (((:) (trace "X" ('G')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('H')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('M')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('.')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('r')) (trace "X" ([])))))))))))))))))))))))))))))))))) (trace "X" ((\hetmet_pga_loopr > (trace "X" ((trace "X" (Prelude.return (trace "X" ((trace "X" ((coqPassCoreToCore' (trace "X" (do_flatten)) (trace "X" (do_skolemize)) (trace "X" (hetmet_brak)) (trace "X" (hetmet_esc)) (trace "X" (uniqueSupply)) (trace "X" (hetmet_PGArrow)) (trace "X" (hetmet_PGArrow_unit)) (trace "X" (hetmet_PGArrow_tensor)) (trace "X" (hetmet_pga_id)) (trace "X" (hetmet_pga_comp)) (trace "X" (hetmet_pga_first)) (trace "X" (hetmet_pga_second)) (trace "X" (hetmet_pga_cancell)) (trace "X" (hetmet_pga_cancelr)) (trace "X" (hetmet_pga_uncancell)) (trace "X" (hetmet_pga_uncancelr)) (trace "X" (hetmet_pga_assoc)) (trace "X" (hetmet_pga_unassoc)) (trace "X" (hetmet_pga_copy)) (trace "X" (hetmet_pga_drop)) (trace "X" (hetmet_pga_swap)) (trace "X" (hetmet_pga_loopl)) (trace "X" (hetmet_pga_loopr)) (trace "X" (lbinds))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

1.7.10.4