remove RLet and RWhere

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index c42842a..1731aad 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -288,7 +288,7 @@ Section HaskFlattener.
     ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant      |- [y]@lev ].
     intros.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    eapply nd_comp; [ idtac | apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -304,7 +304,7 @@ Section HaskFlattener.
       [ Γ > Δ > a                           |- [@ga_mk _ ec y z ]@lev ]
       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
     intros.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ idtac | eapply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -327,7 +327,7 @@ Section HaskFlattener.
       [ Γ > Δ > a                           |- [@ga_mk _ ec x y ]@lev ]
       [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
     intros.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ idtac | eapply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -348,7 +348,7 @@ Section HaskFlattener.
             [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
     intros.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    eapply nd_comp; [ idtac | apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -371,7 +371,7 @@ Section HaskFlattener.
      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
     intros.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    eapply nd_comp; [ idtac | apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -394,12 +394,12 @@ Section HaskFlattener.
      [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b ]@l ].
      intros.
      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
-     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+     eapply nd_comp; [ idtac | eapply RLet ].
      eapply nd_comp; [ apply nd_llecnac | idtac ].
      apply nd_prod.
      apply ga_first.
 
-     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+     eapply nd_comp; [ idtac | eapply RLet ].
      eapply nd_comp; [ apply nd_llecnac | idtac ].
      apply nd_prod.
      apply postcompose.
@@ -450,14 +450,14 @@ Section HaskFlattener.
           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
-          eapply nd_comp; [ idtac | eapply nd_rule; apply
+          eapply nd_comp; [ idtac | apply
              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
           eapply nd_comp; [ apply nd_llecnac | idtac ].
           apply nd_prod.
           apply r2'.
           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
-          eapply nd_comp; [ idtac | eapply nd_rule;  apply RLet ].
+          eapply nd_comp; [ idtac | apply RLet ].
           eapply nd_comp; [ apply nd_llecnac | idtac ].
           eapply nd_prod.
           apply r1'.
@@ -537,13 +537,13 @@ Section HaskFlattener.
     intro pfb.
     apply secondify with (c:=a)  in pfb.
     apply firstify  with (c:=[])  in pfa.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ idtac | eapply RLet ].
     eapply nd_comp; [ eapply nd_llecnac | idtac ].
     apply nd_prod.
     apply pfa.
     clear pfa.
 
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ idtac | eapply RLet ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
@@ -576,7 +576,7 @@ Section HaskFlattener.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
     simpl.
     eapply nd_comp; [ apply nd_llecnac | idtac ].
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ idtac | eapply RLet ].
     apply nd_prod.
     Focus 2.
     apply nd_id.
@@ -643,7 +643,7 @@ Section HaskFlattener.
     simpl.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
     set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    eapply nd_comp; [ idtac | apply RLet ].
     clear q''.
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
@@ -830,11 +830,9 @@ Section HaskFlattener.
       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
-      | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
       | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
       | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
-      | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
       | RVoid    _ _       l           => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
@@ -958,59 +956,6 @@ Section HaskFlattener.
   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
 *)
 
-    destruct case_RLet.
-      simpl.
-      destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
-      repeat drop_simplify.
-      repeat take_simplify.
-      simpl.
-
-      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
-      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
-      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
-      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
-
-      eapply nd_comp.
-      eapply nd_prod; [ idtac | apply nd_id ].
-      eapply boost.
-      apply (ga_first _ _ _ _ _ _ Σ₂').
-
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
-      apply nd_prod.
-      apply nd_id.
-      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
-      apply precompose.
-
-    destruct case_RWhere.
-      simpl.
-      destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
-      repeat take_simplify.
-      repeat drop_simplify.
-      simpl.
-
-      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
-      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
-      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
-      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
-      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
-      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
-
-      eapply nd_comp.
-      eapply nd_prod; [ eapply nd_id | idtac ].
-      eapply (first_nd _ _ _ _ _ _ Σ₃').
-      eapply nd_comp.
-      eapply nd_prod; [ eapply nd_id | idtac ].
-      eapply (second_nd _ _ _ _ _ _ Σ₁').
-
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
-      apply nd_prod; [ idtac | apply nd_id ].
-      eapply nd_comp; [ idtac | eapply precompose' ].
-      apply nd_rule.
-      apply RArrange.
-      apply ALeft.
-      apply ACanL.
-
     destruct case_RCut.
       simpl.
       destruct l as [|ec lev]; simpl.
@@ -1277,7 +1222,7 @@ Section HaskFlattener.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+      eapply nd_comp; [ idtac | eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; [ idtac | eapply boost ].
       induction x.

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 8c6acf4..5e6fac4 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -68,9 +68,6 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 (* 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]
 
-| RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l]
-| RWhere         : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]
-
 | RCut           : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l]
 | RLeft          : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
 | RRight         : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
@@ -109,6 +106,23 @@ Definition RCut'  : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,
   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 :=
@@ -123,7 +137,6 @@ 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_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).
@@ -159,8 +172,6 @@ Lemma no_rules_with_multiple_conclusions : forall c h,
     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.

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 323c1d6..716a983 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -189,11 +189,9 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
-    | RLet          _ _ _ _ _ _ _     => "Let"
     | RCut          _ _ _ _ _ _ _ _   => "Cut"
     | RLeft         _ _ _ _ _ _       => "Left"
     | RRight        _ _ _ _ _ _       => "Right"
-    | RWhere        _ _ _ _ _ _ _ _   => "Where"
     | RLetRec       _ _ _ _ _ _       => "LetRec"
     | RCase         _ _ _ _ _ _ _ _   => "Case"
     | RBrak         _ _ _ _ _ _       => "Brak"

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 8cbebce..0d90d4c 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -763,11 +763,9 @@ Section HaskProofToStrong.
       | RAppCo  Γ Δ Σ κ σ₁ σ₂ γ σ l   => let case_RAppCo := tt        in _
       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
-      | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
       | RCut    Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
       | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
-      | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
       | RVoid   _ _ l                 => let case_RVoid := tt   in _
       | RBrak   Σ a b c n m           => let case_RBrak := tt         in _
       | REsc    Σ a b c n m           => let case_REsc := tt          in _
@@ -869,50 +867,6 @@ Section HaskProofToStrong.
     simpl in *.
     apply (EApp _ _ _ _ _ _ q1' q2').
 
-  destruct case_RLet.
-    eapply rlet.
-    apply X_.
-
-  destruct case_RWhere.
-    apply ILeaf.
-    simpl in *; intros.
-    destruct vars;  try destruct o; inversion H.
-    destruct vars2; try destruct o; inversion H2.
-    clear H2.
-
-    assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
-    refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
-    apply FreshMon.
-
-    destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
-    inversion X_.
-    apply ileaf in X.
-    apply ileaf in X0.
-    simpl in *.
-
-    refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
-    apply FreshMon.
-    simpl.
-    inversion pf1.
-    rewrite H3.
-    rewrite H4.
-    rewrite pf2.
-    reflexivity.
-
-    refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
-    apply FreshMon.
-    reflexivity.
-    apply FreshMon.
-
-    apply ILeaf.
-    apply ileaf in X0'.
-    apply ileaf in X1'.
-    simpl in *.
-    apply ELet with (ev:=vnew)(tv:=σ₁).
-    apply X1'.
-    apply X0'.
-
   destruct case_RCut.
     apply rassoc.
     apply swapr.

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index b1d65e6..435b687 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -231,11 +231,9 @@ Section HaskSkolemizer.
       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
-      | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
       | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
       | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
       | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
-      | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt          in _
       | RVoid    _ _           l       => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
       | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _
@@ -372,56 +370,8 @@ Section HaskSkolemizer.
         eapply take_unarrange.
 
         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
-        eapply nd_rule; eapply SFlat; apply RWhere.
-
-      destruct case_RLet.
-        simpl.
-        destruct lev.
-        apply nd_rule.
-        apply SFlat.
-        apply RLet.
-        set (check_hof σ₁) as hof_tx.
-        destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
-        destruct a.
-        rewrite H.
-        rewrite H0.
-
-        eapply nd_comp.
-        eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | eapply nd_id ].
-
-        set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
-        apply nd_prod.
-          apply nd_id.
-          apply nd_rule.
-          eapply SFlat.
-          eapply RArrange.
-          eapply AuAssoc.
-
-      destruct case_RWhere.
-        simpl.
-        destruct lev.
-        apply nd_rule.
-        apply SFlat.
-        apply RWhere.
-        set (check_hof σ₁) as hof_tx.
-        destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
-        destruct a.
-        rewrite H.
-        rewrite H0.
-
-        eapply nd_comp.
-        eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
-        apply nd_prod; [ idtac | eapply nd_id ].
-        eapply nd_rule; apply SFlat; eapply RArrange.
-        eapply AComp.
-        eapply AuAssoc.
-        apply ALeft.
-        eapply AuAssoc.
+        eapply nd_comp; [ apply nd_exch | idtac ].
+        eapply nd_rule; eapply SFlat; eapply RCut.
 
       destruct case_RCut.
         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ].

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 35373a7..1f1229d 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -1189,7 +1189,7 @@ Definition expr2proof  :
         inversion H.
 
     destruct case_ELet; intros; simpl in *.
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+      eapply nd_comp; [ idtac | eapply RLet ].
       eapply nd_comp; [ apply nd_rlecnac | idtac ].
       apply nd_prod.
       apply pf_let.