+Definition factorContextLeft
+ (Γ: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 ξ ([v],,(stripOutVars (v::nil) ctx)) )).
+
+ 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 RuCanR.
+
+ (* where the leaf is NOT v *)
+ apply inl.
+ apply RuCanL.
+
+ (* empty leaf *)
+ destruct case_None.
+ apply inl; simpl in *.
+ apply RuCanR.
+
+ (* 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.
+ simpl.
+ eapply RComp; [idtac | apply RuCanL ].
+ exact (RComp
+ (* order will not matter because these are central as morphisms *)
+ (RRight _ (RComp lpf (RCanL _)))
+ (RLeft _ (RComp rpf (RCanL _)))).
+
+ destruct case_Right.
+ apply inr.
+ unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
+ fold (stripOutVars (v::nil)).
+ eapply RComp; [ idtac | eapply pivotContext' ].
+ eapply RComp.
+ eapply RRight.
+ eapply RComp.
+ apply lpf.
+ apply RCanL.
+ eapply RLeft.
+ apply rpf.
+
+ destruct case_Left.
+ apply inr.
+ fold (stripOutVars (v::nil)).
+ simpl.
+ eapply RComp.
+ eapply RLeft.
+ eapply RComp.
+ apply rpf.
+ simpl.
+ eapply RCanL.
+ eapply RComp; [ idtac | eapply RCossa ].
+ eapply RRight.
+ apply lpf.
+
+ destruct case_Both.
+ apply inr.
+ simpl.
+ eapply RComp; [ idtac | eapply RRight; eapply RCont ].
+ eapply RComp; [ eapply RRight; eapply lpf | idtac ].
+ eapply RComp; [ eapply RLeft; eapply rpf | idtac ].
+ clear lpf rpf.
+ simpl.
+ apply arrangeSwapMiddle.
+ Defined.
+
+Definition factorContextRight