+manyFresh :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> (Tree (Prelude.Maybe LeveledHaskType)) -> (a1 -> LeveledHaskType) -> FreshM a1 (SigT (Tree (Prelude.Maybe a1)) (SigT (a1 -> LeveledHaskType) ()))
+manyFresh eqdec_vv freshM __U0393_0 __U03a3_ =
+ (trace "X" ((trace "X" (tree_rect (trace "X" ((\a __U03be_0 ->
+ (trace "X" (case (trace "X" (a)) of {
+ Prelude.Just l -> (trace "X" (case (trace "X" (l)) of {
+ MkLeveledHaskType __U03c4_ l0 -> (trace "X" (let {q = (trace "X" ((trace "X" (fresh_lemma' (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03c4_)))))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" (__U03be_0)) (trace "X" (l0))))))} in (trace "X" ((trace "X" (bindM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" (q)) (trace "X" ((\q' -> (trace "X" ((trace "X" (returnM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" ((ExistT (trace "X" ((trace "X" ((mapOptionTree (trace "X" (fst)) (trace "X" (q'))))))) (trace "X" ((ExistT (trace "X" ((trace "X" ((update_xi (trace "X" (eqdec_vv)) (trace "X" (__U0393_0)) (trace "X" (__U03be_0)) (trace "X" (l0)) (trace "X" ((trace "X" ((leaves (trace "X" (q')))))))))))) (trace "X" (__)))))))))))))))))))))}));
+ Prelude.Nothing -> (trace "X" ((trace "X" (returnM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" ((ExistT (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((ExistT (trace "X" (__U03be_0)) (trace "X" (__))))))))))))}))))) (trace "X" ((\__U03a3_1 iH__U03a3_1 __U03a3_2 iH__U03a3_2 __U03be_0 ->
+ (trace "X" ((trace "X" (bindM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" ((trace "X" ((iH__U03a3_1 (trace "X" (__U03be_0))))))) (trace "X" ((\f1 ->
+ (trace "X" (case (trace "X" (f1)) of {
+ ExistT vars1 s ->
+ (trace "X" (case (trace "X" (s)) of {
+ ExistT __U03be_1 _ ->
+ (trace "X" ((trace "X" (bindM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" ((trace "X" ((iH__U03a3_2 (trace "X" (__U03be_1))))))) (trace "X" ((\f2 ->
+ (trace "X" (case (trace "X" (f2)) of {
+ ExistT vars2 s0 -> (trace "X" (case (trace "X" (s0)) of {
+ ExistT __U03be_2 _ -> (trace "X" ((trace "X" (returnM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" ((ExistT (trace "X" ((T_Branch (trace "X" (vars1)) (trace "X" (vars2))))) (trace "X" ((ExistT (trace "X" (__U03be_2)) (trace "X" (__))))))))))))}))})))))))))}))})))))))))))) (trace "X" (__U03a3_))))))
+
+rlet :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> HaskType -> HaskType -> HaskLevel -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+rlet eqdec_vv freshM __U0393_0 __U0394_0 __U03a3___U2081_ __U03a3___U2082_ __U03c3___U2081_ __U03c3___U2082_ p x_ =
+ (trace "X" (ILeaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2082_))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03c3___U2082_)))))))) (trace "X" (p)))))
+ (trace "X" ((unsafeCoerce (trace "X" ((\__U03be_0 vars _ ->
+ (trace "X" (case (trace "X" (vars)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars1 vars2 ->
+ (trace "X" ((trace "X" (bindM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" ((trace "X" ((fresh_lemma (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U03be_0)) (trace "X" (vars2)) (trace "X" (__U03a3___U2082_)) (trace "X" (__U03c3___U2081_)) (trace "X" (p))))))) (trace "X" ((\pf ->
+ (trace "X" (let {__U03be_' = (trace "X" ((trace "X" (update_xi (trace "X" (eqdec_vv)) (trace "X" (__U0393_0)) (trace "X" (__U03be_0)) (trace "X" (p)) (trace "X" (((:) (trace "X" (((,) (trace "X" (pf)) (trace "X" (__U03c3___U2081_))))) (trace "X" (([]))))))))))} in
+ (trace "X" (case (trace "X" (x_)) of {
+ INone -> (trace "X" (false_rect));
+ ILeaf i x -> (trace "X" ((trace "X" (false_rect (trace "X" (x))))));
+ IBranch it1 it2 x x0 -> (trace "X" (let {h = (trace "X" ((trace "X" (eq_rect (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03c3___U2081_)))))))) (trace "X" (p))))))))))) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkLeveledHaskType (trace "X" (__U03c3___U2081_)) (trace "X" (p))))))))))) (trace "X" (__U03a3___U2082_))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03c3___U2082_)))))))) (trace "X" (p))))))))))) (trace "X" ((\x1 x2 -> (trace "X" (let {x3 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03c3___U2081_)))))))) (trace "X" (p))))) (trace "X" (x1))))))} in (trace "X" (let {x4 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkLeveledHaskType (trace "X" (__U03c3___U2081_)) (trace "X" (p))))))))))) (trace "X" (__U03a3___U2082_))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03c3___U2082_)))))))) (trace "X" (p))))) (trace "X" (x2))))))} in (trace "X" ((trace "X" (bindM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" ((trace "X" ((x3 (trace "X" (__U03be_0)) (trace "X" (vars1)) (trace "X" (__))))))) (trace "X" ((\x0' -> (trace "X" ((trace "X" (bindM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" ((trace "X" ((x4 (trace "X" (__U03be_')) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (pf)))))))) (trace "X" (vars2))))) (trace "X" (__))))))) (trace "X" ((\x1' -> (trace "X" ((trace "X" (returnM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" ((ILeaf (trace "X" (__U03c3___U2082_)) (trace "X" ((let {x1'0 = (trace "X" ((trace "X" (ileaf (trace "X" (__U03c3___U2082_)) (trace "X" (x1'))))))} in (trace "X" (let {x0'0 = (trace "X" ((trace "X" (ileaf (trace "X" (__U03c3___U2081_)) (trace "X" (x0'))))))} in (trace "X" (ELet (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03be_0)) (trace "X" (__U03c3___U2081_)) (trace "X" (__U03c3___U2082_)) (trace "X" (p)) (trace "X" (pf)) (trace "X" (x0'0)) (trace "X" (x1'0))))))))))))))))))))))))))))))))))))) (trace "X" (it2))))))))) (trace "X" (it1)) (trace "X" (__))))))} in (trace "X" ((trace "X" (unsafeCoerce (trace "X" (h)) (trace "X" (x)) (trace "X" (x0))))))))})))))))))))}))))))))))
+
+vartree :: (EqDecidable a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe HaskType)) -> HaskLevel -> (a1 -> LeveledHaskType) -> (Tree (Prelude.Maybe a1)) -> ITree HaskType (Expr a1)
+vartree eqdec_vv __U0393_0 __U0394_0 __U03a3_ lev __U03be_0 vars =
+ (trace "X" ((trace "X" (tree_rect (trace "X" ((\a vars0 _ ->
+ (trace "X" (case (trace "X" (a)) of {
+ Prelude.Just h -> (trace "X" (ILeaf (trace "X" (h))
+ (trace "X" ((case (trace "X" (vars0)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just v -> (trace "X" (let {q = (trace "X" (EVar (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03be_0)) (trace "X" (v))))} in (trace "X" ((trace "X" (eq_rect_r (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))) (trace "X" (q)) (trace "X" ((MkLeveledHaskType (trace "X" (h)) (trace "X" (lev)))))))))));
+ Prelude.Nothing -> (trace "X" (false_rect))}));
+ T_Branch vars1 vars2 -> (trace "X" (false_rect))})))));
+ Prelude.Nothing -> (trace "X" (INone))}))))) (trace "X" ((\__U03a3_1 iH__U03a3_1 __U03a3_2 iH__U03a3_2 vars0 _ ->
+ (trace "X" (case (trace "X" (vars0)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars1 vars2 -> (trace "X" (IBranch (trace "X" (__U03a3_1)) (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((iH__U03a3_1 (trace "X" (vars1)) (trace "X" (__))))))) (trace "X" ((trace "X" ((iH__U03a3_2 (trace "X" (vars2)) (trace "X" (__)))))))))}))))) (trace "X" (__U03a3_)) (trace "X" (vars)) (trace "X" (__))))))
+
+rdrop :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe HaskType)) -> (Tree (Prelude.Maybe HaskType)) -> HaskLevel -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+rdrop eqdec_vv freshM __U0393_0 __U0394_0 __U03a3___U2081_ __U03a3___U2081___U2082_ a lev x =
+ (trace "X" (let {x0 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (__U03a3___U2081___U2082_))))) (trace "X" (lev))))) (trace "X" (x))))))} in
+ (trace "X" (ILeaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" (a)) (trace "X" (lev)))))
+ (trace "X" ((unsafeCoerce (trace "X" ((\__U03be_0 vars _ ->
+ (trace "X" (let {q = (trace "X" ((trace "X" (unsafeCoerce (trace "X" (x0)) (trace "X" (__U03be_0)) (trace "X" (vars)) (trace "X" (__))))))} in
+ (trace "X" ((trace "X" (bindM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" (q)) (trace "X" ((\q' ->
+ (trace "X" ((trace "X" (returnM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM)))))))
+ (trace "X" ((case (trace "X" (q')) of {
+ INone -> (trace "X" (false_rect));
+ ILeaf i x1 -> (trace "X" ((trace "X" (false_rect (trace "X" (x1))))));
+ IBranch it1 it2 x1 x2 -> (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (__U03a3___U2081___U2082_)) (trace "X" ((\x3 x4 -> (trace "X" (x3))))) (trace "X" (it2))))))))) (trace "X" (it1)) (trace "X" (__)) (trace "X" (x1)) (trace "X" (x2))))))}))))))))))))))))))))))))))
+
+rdrop' :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe HaskType)) -> (Tree (Prelude.Maybe HaskType)) -> HaskLevel -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+rdrop' eqdec_vv freshM __U0393_0 __U0394_0 __U03a3___U2081_ __U03a3___U2081___U2082_ a lev x =
+ (trace "X" (let {x0 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" ((T_Branch (trace "X" (__U03a3___U2081___U2082_)) (trace "X" (a))))) (trace "X" (lev))))) (trace "X" (x))))))} in
+ (trace "X" (ILeaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" (a)) (trace "X" (lev)))))
+ (trace "X" ((unsafeCoerce (trace "X" ((\__U03be_0 vars _ ->
+ (trace "X" (let {q = (trace "X" ((trace "X" (unsafeCoerce (trace "X" (x0)) (trace "X" (__U03be_0)) (trace "X" (vars)) (trace "X" (__))))))} in
+ (trace "X" ((trace "X" (bindM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM))))))) (trace "X" (q)) (trace "X" ((\q' ->
+ (trace "X" ((trace "X" (returnM (trace "X" ((trace "X" ((freshMon (trace "X" (freshM)))))))
+ (trace "X" ((case (trace "X" (q')) of {
+ INone -> (trace "X" (false_rect));
+ ILeaf i x1 -> (trace "X" ((trace "X" (false_rect (trace "X" (x1))))));
+ IBranch it1 it2 x1 x2 -> (trace "X" ((trace "X" (eq_rect (trace "X" (__U03a3___U2081___U2082_)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\x3 x4 -> (trace "X" (x4))))) (trace "X" (it2))))))))) (trace "X" (it1)) (trace "X" (__)) (trace "X" (x1)) (trace "X" (x2))))))}))))))))))))))))))))))))))
+
+rdrop'' :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe HaskType)) -> HaskLevel -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+rdrop'' eqdec_vv freshM __U0393_0 __U0394_0 __U03a3___U2081_ __U03a3___U2081___U2082_ lev x =
+ (trace "X" (let {x0 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" (__U03a3___U2081_))))) (trace "X" (__U03a3___U2081___U2082_)) (trace "X" (lev))))) (trace "X" (x))))))} in (trace "X" (ILeaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2081___U2082_)) (trace "X" (lev))))) (trace "X" ((unsafeCoerce (trace "X" ((\__U03be_0 vars _ -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (x0)) (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" (vars))))) (trace "X" (__))))))))))))))))
+
+rdrop''' :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe HaskType)) -> HaskLevel -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+rdrop''' eqdec_vv freshM __U0393_0 __U0394_0 a __U03a3___U2081_ __U03a3___U2081___U2082_ lev x =
+ (trace "X" (let {x0 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2081___U2082_)) (trace "X" (lev))))) (trace "X" (x))))))} in
+ (trace "X" (ILeaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (__U03a3___U2081_))))) (trace "X" (__U03a3___U2081___U2082_)) (trace "X" (lev)))))
+ (trace "X" ((unsafeCoerce (trace "X" ((\__U03be_0 vars _ ->
+ (trace "X" (case (trace "X" (vars)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars1 vars2 -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (x0)) (trace "X" (__U03be_0)) (trace "X" (vars2)) (trace "X" (__))))))}))))))))))))
+
+rassoc :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe HaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> HaskLevel -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+rassoc eqdec_vv freshM __U0393_0 __U0394_0 __U03a3___U2081_ a b c lev x =
+ (trace "X" (let {x0 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c))))) (trace "X" (__U03a3___U2081_)) (trace "X" (lev))))) (trace "X" (x))))))} in
+ (trace "X" (ILeaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c)))))))) (trace "X" (__U03a3___U2081_)) (trace "X" (lev)))))
+ (trace "X" ((unsafeCoerce (trace "X" ((\__U03be_0 vars _ ->
+ (trace "X" (case (trace "X" (vars)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars1 vars2 ->
+ (trace "X" (case (trace "X" (vars2)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars2_1 vars2_2 -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (x0)) (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (vars1)) (trace "X" (vars2_1))))) (trace "X" (vars2_2))))) (trace "X" (__))))))}))}))))))))))))
+
+rassoc' :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe HaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> HaskLevel -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+rassoc' eqdec_vv freshM __U0393_0 __U0394_0 __U03a3___U2081_ a b c lev x =
+ (trace "X" (let {x0 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c)))))))) (trace "X" (__U03a3___U2081_)) (trace "X" (lev))))) (trace "X" (x))))))} in
+ (trace "X" (ILeaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c))))) (trace "X" (__U03a3___U2081_)) (trace "X" (lev)))))
+ (trace "X" ((unsafeCoerce (trace "X" ((\__U03be_0 vars _ ->
+ (trace "X" (case (trace "X" (vars)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars1 vars2 ->
+ (trace "X" (case (trace "X" (vars1)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars1_1 vars1_2 -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (x0)) (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" (vars1_1)) (trace "X" ((T_Branch (trace "X" (vars1_2)) (trace "X" (vars2)))))))) (trace "X" (__))))))}))}))))))))))))
+
+swapr :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe HaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> HaskLevel -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+swapr eqdec_vv freshM __U0393_0 __U0394_0 __U03a3___U2081_ a b c lev x =
+ (trace "X" (let {x0 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c))))) (trace "X" (__U03a3___U2081_)) (trace "X" (lev))))) (trace "X" (x))))))} in
+ (trace "X" (ILeaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (a))))) (trace "X" (c))))) (trace "X" (__U03a3___U2081_)) (trace "X" (lev)))))
+ (trace "X" ((unsafeCoerce (trace "X" ((\__U03be_0 vars _ ->
+ (trace "X" (case (trace "X" (vars)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars1 vars2 ->
+ (trace "X" (case (trace "X" (vars1)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars1_1 vars1_2 -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (x0)) (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (vars1_2)) (trace "X" (vars1_1))))) (trace "X" (vars2))))) (trace "X" (__))))))}))}))))))))))))
+
+rdup :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> (Tree (Prelude.Maybe HaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> HaskLevel -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+rdup eqdec_vv freshM __U0393_0 __U0394_0 __U03a3___U2081_ a c lev x =
+ (trace "X" (let {x0 = (trace "X" ((trace "X" (ileaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (a))))) (trace "X" (c))))) (trace "X" (__U03a3___U2081_)) (trace "X" (lev))))) (trace "X" (x))))))} in
+ (trace "X" (ILeaf (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" (__U03a3___U2081_)) (trace "X" (lev)))))
+ (trace "X" ((unsafeCoerce (trace "X" ((\__U03be_0 vars _ ->
+ (trace "X" (case (trace "X" (vars)) of {
+ T_Leaf o -> (trace "X" (false_rect));
+ T_Branch vars1 vars2 -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (x0)) (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (vars1)) (trace "X" (vars1))))) (trace "X" (vars2))))) (trace "X" (__))))))}))))))))))))
+
+rcut :: (EqDecidable a1) -> (FreshMonad a1) -> TypeEnv -> CoercionEnv -> HaskType -> HaskLevel -> (Tree (Prelude.Maybe HaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (Tree (Prelude.Maybe LeveledHaskType)) -> (ITree Judg (Judg2exprType a1)) -> (ITree Judg (Judg2exprType a1)) -> ITree Judg (Judg2exprType a1)
+rcut eqdec_vv freshM __U0393_0 __U0394_0 __U03a3___U2083_ lev __U03a3___U2081___U2082_ =
+ (trace "X" ((trace "X" (tree_rect (trace "X" ((\a __U03a3___U2081_ __U03a3___U2082_ x x0 ->
+ (trace "X" (case (trace "X" (a)) of {
+ Prelude.Just h -> (trace "X" ((trace "X" (rlet (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2082_)) (trace "X" (h)) (trace "X" (__U03a3___U2083_)) (trace "X" (lev)) (trace "X" ((IBranch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (h)))))))) (trace "X" (lev))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkJudg (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((MkLeveledHaskType (trace "X" (h)) (trace "X" (lev))))))))))) (trace "X" (__U03a3___U2082_))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03a3___U2083_)))))))) (trace "X" (lev))))))))))) (trace "X" (x)) (trace "X" (x0)))))))));
+ Prelude.Nothing -> (trace "X" (let {x1 = (trace "X" ((trace "X" (rdrop'' (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2082_)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03a3___U2083_)))))))) (trace "X" (lev)) (trace "X" (x0))))))} in (trace "X" ((trace "X" (rdrop''' (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2082_)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03a3___U2083_)))))))) (trace "X" (lev)) (trace "X" (x1))))))))}))))) (trace "X" ((\__U03a3___U2081___U2082_1 iH__U03a3___U2081___U2082_1 __U03a3___U2081___U2082_2 iH__U03a3___U2081___U2082_2 __U03a3___U2081_ __U03a3___U2082_ x x0 -> (trace "X" (let {x1 = (trace "X" ((trace "X" (rassoc (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03a3___U2083_)))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\t' -> (trace "X" (MkLeveledHaskType (trace "X" (t')) (trace "X" (lev))))))) (trace "X" (__U03a3___U2081___U2082_1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\t' -> (trace "X" (MkLeveledHaskType (trace "X" (t')) (trace "X" (lev))))))) (trace "X" (__U03a3___U2081___U2082_2))))))) (trace "X" (__U03a3___U2082_)) (trace "X" (lev)) (trace "X" (x0))))))} in (trace "X" (let {q = (trace "X" ((trace "X" (iH__U03a3___U2081___U2082_1 (trace "X" (__U03a3___U2081_)) (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\t' -> (trace "X" (MkLeveledHaskType (trace "X" (t')) (trace "X" (lev))))))) (trace "X" (__U03a3___U2081___U2082_2))))))) (trace "X" (__U03a3___U2082_))))) (trace "X" ((trace "X" ((rdrop (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2081___U2082_2)) (trace "X" (__U03a3___U2081___U2082_1)) (trace "X" (lev)) (trace "X" (x))))))) (trace "X" (x1))))))} in (trace "X" (let {q' = (trace "X" ((trace "X" (iH__U03a3___U2081___U2082_2 (trace "X" (__U03a3___U2081_)) (trace "X" ((T_Branch (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2082_))))) (trace "X" ((trace "X" ((rdrop' (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2081___U2082_1)) (trace "X" (__U03a3___U2081___U2082_2)) (trace "X" (lev)) (trace "X" (x)))))))))))} in (trace "X" (let {q0 = (trace "X" ((trace "X" (rassoc' (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03a3___U2083_)))))))) (trace "X" (__U03a3___U2081_)) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\t' -> (trace "X" (MkLeveledHaskType (trace "X" (t')) (trace "X" (lev))))))) (trace "X" (__U03a3___U2081___U2082_2))))))) (trace "X" (__U03a3___U2082_)) (trace "X" (lev)) (trace "X" (q))))))} in (trace "X" (let {q1 = (trace "X" ((trace "X" (swapr (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03a3___U2083_)))))))) (trace "X" (__U03a3___U2081_)) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\t' -> (trace "X" (MkLeveledHaskType (trace "X" (t')) (trace "X" (lev))))))) (trace "X" (__U03a3___U2081___U2082_2))))))) (trace "X" (__U03a3___U2082_)) (trace "X" (lev)) (trace "X" (q0))))))} in (trace "X" (let {q2 = (trace "X" ((trace "X" (rassoc (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03a3___U2083_)))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" ((\t' -> (trace "X" (MkLeveledHaskType (trace "X" (t')) (trace "X" (lev))))))) (trace "X" (__U03a3___U2081___U2082_2))))))) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2082_)) (trace "X" (lev)) (trace "X" (q1))))))} in (trace "X" (let {q'' = (trace "X" ((trace "X" (q' (trace "X" (q2))))))} in (trace "X" (let {q''0 = (trace "X" ((trace "X" (rassoc' (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03a3___U2083_)))))))) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2082_)) (trace "X" (lev)) (trace "X" (q''))))))} in (trace "X" ((trace "X" (rdup (trace "X" (eqdec_vv)) (trace "X" (freshM)) (trace "X" (__U0393_0)) (trace "X" (__U0394_0)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (__U03a3___U2083_)))))))) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2082_)) (trace "X" (lev)) (trace "X" (q''0))))))))))))))))))))))))) (trace "X" (__U03a3___U2081___U2082_))))))
+