X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=5e6fac410aba92eea16973986094f6e6c6040a7f;hp=55b0b032a6f5655002f2729462d42122aeaf96ab;hb=af41ffb1692ae207554342ccdc3bf73abaa75a01;hpb=b3214686b18b2d6f6905394494da8d1c17587bdb

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 55b0b03..5e6fac4 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -10,11 +10,13 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskWeakVars.
 
@@ -28,101 +30,105 @@ Inductive Judg  :=
   forall Γ:TypeEnv,
   forall Δ:CoercionEnv Γ,
   Tree ??(LeveledHaskType Γ ★) ->
-  Tree ??(LeveledHaskType Γ ★) ->
+  Tree ??(HaskType Γ ★) ->
+  HaskLevel Γ ->
   Judg.
-  Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
-
-(* A Uniform Judgment (UJudg) has its environment as a type index; we'll use these to distinguish proofs that have a single,
- * uniform context throughout the whole proof.  Such proofs are important because (1) we can do left and right context
- * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *)
-Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
-  mkUJudg :
-  Tree ??(LeveledHaskType Γ ★) ->
-  Tree ??(LeveledHaskType Γ ★) ->
-  UJudg Γ Δ.
-  Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
-  Definition ext_tree_left  {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end).
-  Definition ext_tree_right {Γ}{Δ}  := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end).
-
-(* we can turn a UJudg into a Judg by simply internalizing the index *)
-Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
-  match ej with mkUJudg t s => Γ > Δ > t |- s end.
-  Coercion UJudg2judg : UJudg >-> Judg.
+  Notation "Γ > Δ > a '|-' s '@' l" := (mkJudg Γ Δ a s l) (at level 52, Δ at level 50, a at level 52, s at level 50, l at level 50).
 
 (* information needed to define a case branch in a HaskProof *)
 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
 { pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
-; pcb_judg           := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ)
+; pcb_judg           := sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ)
                 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
                   (vec2list (sac_types sac Γ avars))))
-                |- [weakLT' (branchtype @@ lev)]
+                |- [weakT' branchtype ] @ weakL' lev
 }.
-(*Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.*)
 Implicit Arguments ProofCaseBranch [ ].
 
-(* Figure 3, production $\vdash_E$, Uniform rules *)
-Inductive URule {Γ}{Δ} : Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
-| RCanL   : ∀ t a        ,                          URule  [Γ>>Δ>    [],,a   |- t         ]      [Γ>>Δ>       a   |- t           ]
-| RCanR   : ∀ t a        ,                          URule  [Γ>>Δ>    a,,[]   |- t         ]      [Γ>>Δ>       a   |- t           ]
-| RuCanL  : ∀ t a        ,                          URule  [Γ>>Δ>       a    |- t         ]      [Γ>>Δ>  [],,a    |- t           ]
-| RuCanR  : ∀ t a        ,                          URule  [Γ>>Δ>       a    |- t         ]      [Γ>>Δ>  a,,[]    |- t           ]
-| RAssoc  : ∀ t a b c    ,                          URule  [Γ>>Δ>a,,(b,,c)   |- t         ]      [Γ>>Δ>(a,,b),,c  |- t           ]
-| RCossa  : ∀ t a b c    ,                          URule  [Γ>>Δ>(a,,b),,c   |- t         ]      [Γ>>Δ> a,,(b,,c) |- t           ]
-| RLeft   : ∀ h c x      ,             URule h c -> URule (mapOptionTree (ext_tree_left  x) h) (mapOptionTree (ext_tree_left  x) c)
-| RRight  : ∀ h c x      ,             URule h c -> URule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
-| RExch   : ∀ t a b      ,                          URule  [Γ>>Δ>   (b,,a)   |- t         ]      [Γ>>Δ>  (a,,b)   |- t           ]
-| RWeak   : ∀ t a        ,                          URule  [Γ>>Δ>       []   |- t         ]      [Γ>>Δ>       a   |- t           ]
-| RCont   : ∀ t a        ,                          URule  [Γ>>Δ>  (a,,a)    |- t         ]      [Γ>>Δ>       a   |- t           ].
-
-
 (* Figure 3, production $\vdash_E$, all rules *)
 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
-| RURule  : ∀ Γ Δ h c,                  @URule Γ Δ h c -> Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
+| RArrange  : ∀ Γ Δ Σ₁ Σ₂ Σ l,       Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁     |- Σ            @l]   [Γ > Δ > Σ₂    |- Σ            @l]
 
 (* λ^α rules *)
-| RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t  @@ (v::l) ]]   [Γ > Δ > Σ     |- [<[v|-t]>   @@l]]
-| REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [<[v|-t]> @@ l]]   [Γ > Δ > Σ     |- [t  @@ (v::l)  ]]
+| RBrak : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ      |- [t]@(v::l)     ]   [Γ > Δ > Σ     |- [<[v|-t]>   ] @l]
+| REsc  : ∀ Γ Δ t v Σ l,                              Rule [Γ > Δ > Σ     |- [<[v|-t]>   ] @l]   [Γ > Δ > Σ     |- [t]@(v::l)      ]
 
 (* Part of GHC, but not explicitly in System FC *)
-| RNote   : ∀ Γ Δ Σ τ l,          Note ->             Rule  [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@ l]]
-| RLit    : ∀ Γ Δ v       l,                          Rule  [                                ]   [Γ > Δ > []|- [literalType v @@ l]]
+| RNote   : ∀ Γ Δ Σ τ l,          Note ->             Rule [Γ > Δ > Σ      |- [τ        ]  @l]   [Γ > Δ > Σ     |- [τ          ] @l]
+| RLit    : ∀ Γ Δ v       l,                          Rule [                                 ]   [Γ > Δ > []|- [literalType v ]  @l]
 
 (* SystemFC rules *)
-| RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
-| RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
-| RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
+| RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          ] @l]
+| RGlobal : forall Γ Δ l   (g:Global Γ) v,            Rule [                                 ]   [Γ>Δ>     []   |- [g v        ] @l]
+| RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te]         @l]   [Γ>Δ>    Σ     |- [tx--->te   ] @l]
 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
-HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
- Rule [Γ>Δ> Σ         |- [σ₁@@l]         ]   [Γ>Δ>    Σ     |- [σ₂          @@l]]
-| RBindingGroup  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
-| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
-| RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]
-| REmptyGroup    : ∀ Γ Δ ,               Rule [] [Γ > Δ > [] |- [] ]
-| RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ @@l]]      [Γ>Δ>    Σ     |- [substT σ τ @@l]]
+                   HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->      Rule [Γ>Δ> Σ         |- [σ₁]         @l]   [Γ>Δ>    Σ     |- [σ₂         ] @l]
+
+(* order is important here; we want to be able to skolemize without introducing new AExch'es *)
+| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l])  [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
+
+| RCut           : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l]
+| RLeft          : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
+| RRight         : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
+
+| RVoid    : ∀ Γ Δ l,               Rule [] [Γ > Δ > [] |- [] @l ]
+
+| RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ]@l]      [Γ>Δ>    Σ     |- [substT σ τ]@l]
 | RAbsT   : ∀ Γ Δ Σ κ σ   l,
-  Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
-       [Γ>Δ            >    Σ     |- [HaskTAll κ σ   @@ l]]
+  Rule [(κ::Γ)> (weakCE Δ)    >   mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)]
+       [Γ>Δ            >    Σ     |- [HaskTAll κ σ   ]@l]
+
 | RAppCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
-    Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ>    Σ     |- [σ        @@l]]
+    Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ]@l] [Γ>Δ>    Σ     |- [σ        ]@l]
 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
-   Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
-        [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
-| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
+   Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ ]@l]
+        [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
+
+| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
 | RCase          : forall Γ Δ lev tc Σ avars tbranches
   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
                    Rule
                        ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
-                        [Γ > Δ >                                              Σ |- [ caseType tc avars @@ lev ] ])
-                        [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches         @@ lev ] ]
+                        [Γ > Δ >                                              Σ |- [ caseType tc avars  ] @lev])
+                        [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
 .
-Coercion RURule : URule >-> Rule.
 
+Definition RCut'  : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,
+  ND Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l].
+  intros.
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+  apply nd_prod.
+  apply nd_id.
+  apply nd_rule.
+  apply RArrange.
+  apply AuCanL.
+  Defined.
+
+Definition RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,
+  ND Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l].
+  intros.
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
+  eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+  apply nd_prod.
+  apply nd_id.
+  eapply nd_rule; eapply RArrange; eapply AuCanL.
+  Defined.
+
+Definition RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,
+  ND Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l].
+  intros.
+  eapply nd_comp; [ apply nd_exch | idtac ].
+  eapply nd_rule; eapply RCut.
+  Defined.
 
 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
+(* TODO: change this to (if RBrak/REsc -> False) *)
 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
-| Flat_RURule           : ∀ Γ Δ  h c r            ,  Rule_Flat (RURule Γ Δ  h c r)
+| Flat_RArrange         : ∀ Γ Δ  h c r          a l ,  Rule_Flat (RArrange Γ Δ h c r a l)
 | Flat_RNote            : ∀ Γ Δ Σ τ l n            ,  Rule_Flat (RNote Γ Δ Σ τ l n)
+| Flat_RLit             : ∀ Γ Δ Σ τ               ,  Rule_Flat (RLit Γ Δ Σ τ  )
 | Flat_RVar             : ∀ Γ Δ  σ               l,  Rule_Flat (RVar Γ Δ  σ         l)
 | Flat_RLam             : ∀ Γ Δ  Σ tx te    q    ,  Rule_Flat (RLam Γ Δ  Σ tx te      q )
 | Flat_RCast            : ∀ Γ Δ  Σ σ τ γ    q     ,  Rule_Flat (RCast Γ Δ  Σ σ τ γ    q )
@@ -131,57 +137,13 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 | Flat_RAppCo           : ∀ Γ Δ  Σ σ₁ σ₂ σ γ q l,  Rule_Flat (RAppCo Γ Δ  Σ  σ₁ σ₂ σ γ  q l)
 | Flat_RAbsCo           : ∀ Γ   Σ κ σ  σ₁ σ₂ q1 q2   , Rule_Flat (RAbsCo Γ   Σ κ σ  σ₁ σ₂  q1 q2   )
 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
-| Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
-| Flat_RBindingGroup    : ∀ q a b c d e ,  Rule_Flat (RBindingGroup q a b c d e)
-| Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x).
-
-(* 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.
-
-Lemma no_urules_with_empty_conclusion : forall Γ Δ c h, @URule Γ Δ c h -> h=[] -> False.
-  intro.
-  intro.
-  induction 1; intros; inversion H.
-  simpl in *;  destruct c; try destruct o;  simpl in *; try destruct u;  inversion H;  simpl in *;  apply IHX;  auto;  inversion H1.
-  simpl in *;  destruct c; try destruct o;  simpl in *; try destruct u;  inversion H;  simpl in *;  apply IHX;  auto;  inversion H1.
-  Qed.
+| 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.
-  apply no_urules_with_empty_conclusion in u.
-  apply u.
-  auto.
-  Qed.
-
-Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h,
-  @URule Γ Δ c h -> { h1:Tree ??(UJudg Γ Δ) & { h2:Tree ??(UJudg Γ Δ) & h=(h1,,h2) }} -> False.
-  intro.
-  intro.
-  induction 1; intros.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-
-  apply IHX.
-  destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
-    inversion e.
-    inversion e.
-    exists c1. exists c2. auto.
-
-  apply IHX.
-  destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
-    inversion e.
-    inversion e.
-    exists c1. exists c2. auto.
-
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
-  inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
   Qed.
 
 Lemma no_rules_with_multiple_conclusions : forall c h,
@@ -191,7 +153,7 @@ Lemma no_rules_with_multiple_conclusions : forall c h,
     try apply no_urules_with_empty_conclusion in u; try apply u.
     destruct X0; destruct s; inversion e.
     auto.
-    apply (no_urules_with_multiple_conclusions _ _ h (c1,,c2)) in u. inversion u. exists c1. exists c2. 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.
@@ -221,4 +183,3 @@ Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), Fa
   auto.
   Qed.
 
-