+factorContextLeft :: (EqDecidable a1) -> TypeEnv -> CoercionEnv -> a1 -> (Tree (Prelude.Maybe a1)) -> (a1 -> LeveledHaskType) -> Prelude.Either (Arrange LeveledHaskType) (Arrange LeveledHaskType)
+factorContextLeft eqd_vv __U0393_0 __U0394_0 v ctx __U03be_0 =
+ (trace "X" ((trace "X" (tree_rect (trace "X" ((\a ->
+ (trace "X" (case (trace "X" (a)) of {
+ Prelude.Just v' ->
+ (trace "X" (let {s = (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v')) (trace "X" (v))))))} in
+ (trace "X" (case (trace "X" (s)) of {
+ Prelude.True -> (trace "X" ((trace "X" (eq_rect_r (trace "X" (v)) (trace "X" ((Prelude.Right (trace "X" ((RuCanR (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))))))))) (trace "X" (v'))))));
+ Prelude.False -> (trace "X" (Prelude.Left (trace "X" ((RuCanL (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v'))))))))))))))))))}))));
+ Prelude.Nothing -> (trace "X" (Prelude.Left (trace "X" ((RuCanR (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))))))))}))))) (trace "X" ((\ctx1 iHctx1 ctx2 iHctx2 ->
+ (trace "X" (case (trace "X" (iHctx1)) of {
+ Prelude.Left lpf ->
+ (trace "X" (case (trace "X" (iHctx2)) of {
+ Prelude.Left rpf -> (trace "X" (Prelude.Left (trace "X" ((RComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((RComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1)))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2))))))))))))))) (trace "X" ((RRight (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1)))))))
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1)))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2))))))) (trace "X" ((RComp (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1)))))))))))))))
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1)))))))))))) (trace "X" (lpf)) (trace "X" ((RCanL
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1))))))))))))))))))))) (trace "X" ((RLeft (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2))))))))))))
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1)))))))))))) (trace "X" ((RComp (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2)))))))))))))))
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2)))))))))))) (trace "X" (rpf)) (trace "X" ((RCanL
+ (trace "X" ((trace "X" ((let {
+ mapOptionTree0 f t =
+ (trace "X" (case (trace "X" (t)) of {
+ T_Leaf o ->
+ (trace "X" (case (trace "X" (o)) of {
+ Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
+ Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
+ 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" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2)))))))))))))))))))))))) (trace "X" ((RuCanL (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))))))));
+ Prelude.Right rpf -> (trace "X" (Prelude.Right (trace "X" ((RComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1)))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((RComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1)))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1)))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((RRight (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1)))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2))))))) (trace "X" ((RComp (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1))))))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1)))))))))))) (trace "X" (lpf)) (trace "X" ((RCanL (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1))))))))))))))))))))) (trace "X" ((RLeft (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1)))))))))))) (trace "X" (rpf))))))))
+ (trace "X" ((trace "X" ((pivotContext'
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1)))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2))))))))))))))))))))))}));
+ Prelude.Right lpf ->
+ (trace "X" (case (trace "X" (iHctx2)) of {
+ Prelude.Left rpf -> (trace "X" (Prelude.Right (trace "X" ((RComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((RLeft (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2)))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((RComp (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2))))))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2)))))))))))) (trace "X" (rpf)) (trace "X" ((RCanL (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2))))))))))))))))))))) (trace "X" ((RComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1)))))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((RRight (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1)))))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))) (trace "X" (lpf))))) (trace "X" ((RCossa (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))))))));
+ Prelude.Right rpf -> (trace "X" (Prelude.Right (trace "X" ((RComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((RComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (v)))))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1))))))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((RRight (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (v)))))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1))))))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2))))))) (trace "X" (lpf))))) (trace "X" ((RComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (v)))))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1))))))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2)))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (v)))))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1))))))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (v)))))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2)))))))))))))))))) (trace "X" ((RLeft (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" (ctx2))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (v)))))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx2))))))))))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0)) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (v)))))))) (trace "X" ((trace "X" ((stripOutVars (trace "X" (eqd_vv)) (trace "X" (((:) (trace "X" (v)) (trace "X" (([])))))) (trace "X" (ctx1))))))))))))))) (trace "X" (rpf)))))
+ (trace "X" ((trace "X" ((arrangeSwapMiddle (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1)))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2))))))))))))))))))))))) (trace "X" ((RRight (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v)))))))))))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))) (trace "X" ((T_Branch
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx1))))))))))))
+ (trace "X" ((trace "X" ((mapOptionTree (trace "X" (__U03be_0))
+ (trace "X" ((trace "X" ((mapOptionTree' (trace "X" ((\v0 ->
+ (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqd_vv)) (trace "X" (v0)) (trace "X" (v)))))) of {
+ Prelude.True -> (trace "X" (Prelude.Nothing));
+ Prelude.False -> (trace "X" (Prelude.Just (trace "X" (v0))))}))))) (trace "X" (ctx2))))))))))))))) (trace "X" ((RCont (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((__U03be_0 (trace "X" (v))))))))))))))))))))))))}))}))))) (trace "X" (ctx))))))
+
+factorContextRight :: (EqDecidable a1) -> TypeEnv -> CoercionEnv -> a1 -> (Tree (Prelude.Maybe a1)) -> (a1 -> LeveledHaskType) -> Prelude.Either (Arrange LeveledHaskType) (Arrange LeveledHaskType)
+factorContextRight eqd_vv __U0393_0 __U0394_0 v ctx __U03be_0 =