+| Flat_RJoin : ∀ q a b c d e , Rule_Flat (RJoin q a b c d e)
+| Flat_RVoid : ∀ q a , Rule_Flat (RVoid q a)
+| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
+| Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
+
+Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
+ intros.
+ destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
+ Qed.
+
+Lemma no_rules_with_multiple_conclusions : forall c h,
+ Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
+ intros.
+ destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
+ try apply no_urules_with_empty_conclusion in u; try apply u.
+ destruct X0; destruct s; inversion e.
+ auto.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ destruct X0; destruct s; inversion e.
+ Qed.
+
+Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
+ intros.
+ eapply no_rules_with_multiple_conclusions.
+ apply r.
+ exists c1.
+ exists c2.
+ auto.
+ Qed.
+
+(* "Arrange" objects are parametric in the type of the leaves of the tree *)
+Definition arrangeMap :
+ forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
+ Arrange Σ₁ Σ₂ ->
+ Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
+ intros.
+ induction X; simpl.
+ apply RId.
+ apply RCanL.
+ apply RCanR.
+ apply RuCanL.
+ apply RuCanR.
+ apply RAssoc.
+ apply RCossa.
+ apply RExch.
+ apply RWeak.
+ apply RCont.
+ apply RLeft; auto.
+ apply RRight; auto.
+ eapply RComp; [ apply IHX1 | apply IHX2 ].
+ Defined.
+
+(* a frequently-used Arrange *)
+Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
+ Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
+ eapply RComp.
+ apply RCossa.
+ eapply RComp.
+ eapply RLeft.
+ eapply RComp.
+ eapply RAssoc.
+ eapply RRight.
+ apply RExch.
+ eapply RComp.
+ eapply RLeft.
+ eapply RCossa.
+ eapply RAssoc.
+ Defined.