+ (* if a tree is empty, we can Arrange it to [] *)
+ Definition arrangeCancelEmptyTree : forall {T}{A}(q:Tree A)(t:Tree ??T),
+ t = mapTree (fun _:A => None) q ->
+ Arrange t [].
+ intros T A q.
+ induction q; intros.
+ simpl in H.
+ rewrite H.
+ apply RId.
+ simpl in *.
+ destruct t; try destruct o; inversion H.
+ set (IHq1 _ H1) as x1.
+ set (IHq2 _ H2) as x2.
+ eapply RComp.
+ eapply RRight.
+ rewrite <- H1.
+ apply x1.
+ eapply RComp.
+ apply RCanL.
+ rewrite <- H2.
+ apply x2.
+ Defined.
+
+ (* if a tree is empty, we can Arrange it from [] *)
+ Definition arrangeUnCancelEmptyTree : forall {T}{A}(q:Tree A)(t:Tree ??T),
+ t = mapTree (fun _:A => None) q ->
+ Arrange [] t.
+ intros T A q.
+ induction q; intros.
+ simpl in H.
+ rewrite H.
+ apply RId.
+ simpl in *.
+ destruct t; try destruct o; inversion H.
+ set (IHq1 _ H1) as x1.
+ set (IHq2 _ H2) as x2.
+ eapply RComp.
+ apply RuCanL.
+ eapply RComp.
+ eapply RRight.
+ apply x1.
+ eapply RComp.
+ eapply RLeft.
+ apply x2.
+ rewrite H.
+ apply RId.
+ Defined.
+
+ (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (dropT Σ₁) to (dropT Σ₂) *)
+ Lemma arrangeDrop {T} pred
+ : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (dropT (mkFlags pred Σ₁)) (dropT (mkFlags pred Σ₂)).
+
+ refine ((fix arrangeTake t1 t2 (arr:Arrange t1 t2) :=
+ match arr as R in Arrange A B return Arrange (dropT (mkFlags pred A)) (dropT (mkFlags pred B)) with
+ | RId a => let case_RId := tt in RId _
+ | RCanL a => let case_RCanL := tt in _
+ | RCanR a => let case_RCanR := tt in _
+ | RuCanL a => let case_RuCanL := tt in _
+ | RuCanR a => let case_RuCanR := tt in _
+ | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
+ | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
+ | RExch a b => let case_RExch := tt in RExch _ _
+ | RWeak a => let case_RWeak := tt in _
+ | RCont a => let case_RCont := tt in _
+ | RLeft a b c r' => let case_RLeft := tt in RLeft _ (arrangeTake _ _ r')
+ | RRight a b c r' => let case_RRight := tt in RRight _ (arrangeTake _ _ r')
+ | RComp a b c r1 r2 => let case_RComp := tt in RComp (arrangeTake _ _ r1) (arrangeTake _ _ r2)
+ end)); clear arrangeTake; intros.
+
+ destruct case_RCanL.
+ simpl; destruct (pred None); simpl; apply RCanL.
+
+ destruct case_RCanR.
+ simpl; destruct (pred None); simpl; apply RCanR.
+
+ destruct case_RuCanL.
+ simpl; destruct (pred None); simpl; apply RuCanL.
+
+ destruct case_RuCanR.
+ simpl; destruct (pred None); simpl; apply RuCanR.
+
+ destruct case_RWeak.
+ simpl; destruct (pred None); simpl; apply RWeak.
+
+ destruct case_RCont.
+ simpl; destruct (pred None); simpl; apply RCont.
+
+ Defined.
+
+ (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (takeT Σ₁) to (takeT Σ₂) *)
+ (*
+ Lemma arrangeTake {T} pred
+ : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (takeT' (mkFlags pred Σ₁)) (takeT' (mkFlags pred Σ₂)).
+ unfold takeT'.
+ *)
+