-| Flat_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e)
-| Flat_RCase : ∀ Σ Γ T κlen κ θ l x q, Rule_Flat (RCase Σ Γ T κlen κ θ l x q).
-
-(* given a proof that uses only uniform rules, we can produce a general proof *)
-Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
- := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c.
-
+| Flat_RJoin : ∀ q a b c d e l, Rule_Flat (RJoin q a b c d e l)
+| Flat_RVoid : ∀ q a l, Rule_Flat (RVoid q a l)
+| 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.
+ 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.