+(* same as before, but use AWeak if necessary *)
+Definition factorContextLeftAndWeaken
+ (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+ v (* variable to be pivoted, if found *)
+ ctx (* initial context *)
+ (ξ:VV -> LeveledHaskType Γ ★) :
+ Arrange
+ (mapOptionTree ξ ctx )
+ (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ).
+ set (factorContextLeft Γ Δ v ctx ξ) as q.
+ destruct q; auto.
+ eapply AComp; [ apply a | idtac ].
+ refine (ARight _ (AWeak _)).
+ Defined.
+
+Definition factorContextLeftAndWeaken''
+ (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+ v (* variable to be pivoted, if found *)
+ (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
+ distinct (leaves v) ->
+ Arrange
+ ((mapOptionTree ξ ctx) )
+ ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))).
+
+ induction v; intros.
+ destruct a.
+ unfold mapOptionTree in *.
+ simpl in *.
+ fold (mapOptionTree ξ) in *.
+ intros.
+ set (@factorContextLeftAndWeaken) as q.
+ simpl in q.
+ apply q.
+ apply Δ.
+
+ unfold mapOptionTree; simpl in *.
+ intros.
+ rewrite (@stripping_nothing_is_inert Γ); auto.
+ apply AuCanL.
+ intros.
+ unfold mapOptionTree in *.
+ simpl in *.
+ fold (mapOptionTree ξ) in *.
+ set (mapOptionTree ξ) as X in *.
+
+ set (distinct_app _ _ _ H) as H'.
+ destruct H' as [H1 H2].
+
+ set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'.
+
+ unfold X in *.
+ simpl in *.
+ rewrite <- strip_twice_lemma.
+ set (notin_strip_inert' v2 (leaves v1)) as q.
+ unfold stripOutVars in q.
+ rewrite q in IHv1'.
+ clear q.
+ eapply AComp; [ idtac | eapply AAssoc ].
+ eapply AComp; [ idtac | eapply IHv1' ].
+ clear IHv1'.
+ apply IHv2; auto.
+ auto.
+ auto.
+ Defined.
+
+(* same as before, but use AWeak if necessary *)
+Definition factorContextRightAndWeaken