+ (ARight _ (AComp lpf (ACanL _)))
+ (ALeft _ (AComp rpf (ACanL _)))).
+
+ destruct case_Right.
+ apply inr.
+ unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
+ fold (stripOutVars (v::nil)).
+ eapply AComp; [ idtac | eapply pivotContext' ].
+ eapply AComp.
+ eapply ARight.
+ eapply AComp.
+ apply lpf.
+ apply ACanL.
+ eapply ALeft.
+ apply rpf.
+
+ destruct case_Left.
+ apply inr.
+ fold (stripOutVars (v::nil)).
+ simpl.
+ eapply AComp.
+ eapply ALeft.
+ eapply AComp.
+ apply rpf.
+ simpl.
+ eapply ACanL.
+ eapply AComp; [ idtac | eapply AuAssoc ].
+ eapply ARight.
+ apply lpf.
+
+ destruct case_Both.
+ apply inr.
+ simpl.
+ eapply AComp; [ idtac | eapply ARight; eapply ACont ].
+ eapply AComp; [ eapply ARight; eapply lpf | idtac ].
+ eapply AComp; [ eapply ALeft; eapply rpf | idtac ].
+ clear lpf rpf.
+ simpl.
+ apply arrangeSwapMiddle.
+ Defined.
+
+Definition factorContextRight
+ (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+ v (* variable to be pivoted, if found *)
+ ctx (* initial context *)
+ (ξ:VV -> LeveledHaskType Γ ★)
+ :
+
+ (* a proof concluding in a context where that variable does not appear *)
+ sum (Arrange
+ (mapOptionTree ξ ctx )
+ (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] ))
+
+ (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
+ (Arrange
+ (mapOptionTree ξ ctx )
+ (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) )).
+
+ induction ctx.
+
+ refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
+
+ (* nonempty leaf *)
+ destruct case_Some.
+ unfold stripOutVars in *; simpl.
+ unfold dropVar.
+ unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
+
+ destruct (eqd_dec v' v); subst.
+
+ (* where the leaf is v *)
+ apply inr.
+ subst.
+ apply AuCanL.
+
+ (* where the leaf is NOT v *)
+ apply inl.
+ apply AuCanR.
+
+ (* empty leaf *)
+ destruct case_None.
+ apply inl; simpl in *.
+ apply AuCanR.
+
+ (* branch *)
+ refine (
+ match IHctx1 with
+ | inr lpf =>
+ match IHctx2 with
+ | inr rpf => let case_Both := tt in _
+ | inl rpf => let case_Left := tt in _
+ end
+ | inl lpf =>
+ match IHctx2 with
+ | inr rpf => let case_Right := tt in _
+ | inl rpf => let case_Neither := tt in _
+ end
+ end); clear IHctx1; clear IHctx2.
+
+ destruct case_Neither.
+ apply inl.
+ eapply AComp; [idtac | apply AuCanR ].
+ exact (AComp
+ (* order will not matter because these are central as morphisms *)
+ (ARight _ (AComp lpf (ACanR _)))
+ (ALeft _ (AComp rpf (ACanR _)))).