src/HaskSkolemizer.v

   1 (*********************************************************************************************************************************)
   2 (* HaskSkolemizer:                                                                                                               *)
   3 (*                                                                                                                               *)
   4 (*   Skolemizes the portion of a proof which uses judgments at level >0                                                          *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import NaturalDeductionContext.
  13 Require Import Coq.Strings.String.
  14 Require Import Coq.Lists.List.
  15
  16 Require Import HaskKinds.
  17 Require Import HaskCoreTypes.
  18 Require Import HaskCoreVars.
  19 Require Import HaskWeakTypes.
  20 Require Import HaskWeakVars.
  21 Require Import HaskLiterals.
  22 Require Import HaskTyCons.
  23 Require Import HaskStrongTypes.
  24 Require Import HaskProof.
  25 Require Import NaturalDeduction.
  26
  27 Require Import HaskStrongTypes.
  28 Require Import HaskStrong.
  29 Require Import HaskProof.
  30 Require Import HaskStrongToProof.
  31 Require Import HaskProofToStrong.
  32 Require Import HaskWeakToStrong.
  33
  34 Open Scope nd_scope.
  35 Set Printing Width 130.
  36
  37 Section HaskSkolemizer.
  38
  39 (*
  40   Fixpoint debruijn2phoas {κ} (exp: RawHaskType (fun _ => nat) κ) : HaskType TV κ :=
  41      match exp with
  42     | TVar    _  x          => x
  43     | TAll     _ y          => TAll   _  (fun v => debruijn2phoas  (y (TVar v)))
  44     | TApp   _ _ x y        => TApp      (debruijn2phoas  x) (debruijn2phoas  y)
  45     | TCon       tc         => TCon      tc
  46     | TCoerc _ t1 t2 t      => TCoerc    (debruijn2phoas  t1) (debruijn2phoas  t2)   (debruijn2phoas  t)
  47     | TArrow                => TArrow
  48     | TCode      v e        => TCode     (debruijn2phoas  v) (debruijn2phoas  e)
  49     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (debruijn2phoasyFunApp _ lt)
  50     end
  51     with debruijn2phoasyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun _ => nat) lk) : @HaskTypeList TV lk :=
  52     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
  53     | TyFunApp_nil               => TyFunApp_nil
  54     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (debruijn2phoas  t) (debruijn2phoasyFunApp _ rest)
  55     end.
  56 *)
  57   Definition isNotBrakOrEsc {h}{c} (r:Rule h c) : Prop :=
  58     match r with
  59       | RBrak _ _ _ _ _ _ => False
  60       | REsc  _ _ _ _ _ _ => False
  61       | _                 => True
  62     end.
  63
  64   Fixpoint mkArrows {Γ}(lt:list (HaskType Γ ★))(t:HaskType Γ ★) : HaskType Γ ★ :=
  65     match lt with
  66       | nil => t
  67       | a::b => mkArrows b (a ---> t)
  68     end.
  69
  70 (*
  71   Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
  72     match l with
  73       | nil  => t
  74       | a::b => unleaves_ (t,,[a @@ lev]) b lev
  75     end.
  76 *)
  77   (* weak inverse of "leaves" *)
  78   Fixpoint unleaves_ {A:Type}(l:list A) : Tree (option A) :=
  79     match l with
  80       | nil      => []
  81       | (a::nil) => [a]
  82       | (a::b)   => [a],,(unleaves_ b)
  83     end.
  84
  85   (* rules of skolemized proofs *)
  86   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ @ _ => Γ end.
  87
  88   Fixpoint take_trustme {Γ}
  89     (n:nat)
  90     (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
  91     : list (HaskType Γ ★) :=
  92
  93     match n with
  94       | 0    => nil
  95       | S n' => (fun TV ite => match l TV ite with
  96                 | nil  => Prelude_error "impossible"
  97                 | a::b => a
  98                 end)
  99                 ::
 100                 take_trustme n' (fun TV ite => match l TV ite with
 101                 | nil  => Prelude_error "impossible"
 102                 | a::b => b
 103                 end)
 104     end.
 105
 106   Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
 107     (forall tv ite, f tv ite = g tv ite) -> f=g.
 108
 109   Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
 110     unleaves_
 111     (take_trustme
 112       (count_arg_types (ht _ (ite_unit _)))
 113       (fun TV ite => take_arg_types (ht TV ite))).
 114
 115   Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
 116     fun TV ite => drop_arg_types (ht TV ite).
 117
 118   Implicit Arguments take_arg_types_as_tree [[Γ]].
 119   Implicit Arguments drop_arg_types_as_tree [[Γ]].
 120
 121   Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
 122     Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev)
 123       (take_arg_types_as_tree (tx ---> te) @@@ lev).
 124     intros.
 125     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
 126       rewrite <- e.
 127       simpl.
 128       apply AId.
 129     unfold take_arg_types_as_tree.
 130       Opaque take_arg_types_as_tree.
 131       simpl.
 132       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
 133       simpl.
 134       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
 135       apply ACanR.
 136         apply phoas_extensionality.
 137         reflexivity.
 138     apply (Prelude_error "should not be possible").
 139     Defined.
 140     Transparent take_arg_types_as_tree.
 141
 142   Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
 143     Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
 144       ([tx @@ lev],,take_arg_types_as_tree te @@@ lev).
 145     intros.
 146     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
 147       rewrite <- e.
 148       simpl.
 149       apply AId.
 150     unfold take_arg_types_as_tree.
 151       Opaque take_arg_types_as_tree.
 152       simpl.
 153       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
 154       simpl.
 155       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
 156       apply AuCanR.
 157         apply phoas_extensionality.
 158         reflexivity.
 159     apply (Prelude_error "should not be possible").
 160     Defined.
 161     Transparent take_arg_types_as_tree.
 162
 163   Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
 164     drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
 165     intros.
 166     unfold drop_arg_types_as_tree.
 167     simpl.
 168     reflexivity.
 169     Qed.
 170
 171   Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
 172 (*  | SFlat  : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
 173   | SFlat  : forall h c, Rule h c -> SRule h c
 174   | SBrak  : forall Γ Δ t ec Σ l,
 175     SRule
 176     [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        ] @ (ec::l)]
 177     [Γ > Δ > Σ                                  |- [<[ec |- t]>                ] @l]
 178
 179   | SEsc   : forall Γ Δ t ec Σ l,
 180     SRule
 181     [Γ > Δ > Σ                                  |- [<[ec |- t]>                ] @l]
 182     [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t         ] @ (ec::l)]
 183     .
 184
 185   Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
 186     match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
 187
 188   Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
 189     match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
 190
 191   Definition skolemize_judgment (j:Judg) : Judg :=
 192     match j with
 193       | Γ > Δ > Σ₁ |- Σ₂ @ nil       => j
 194         | Γ > Δ > Σ₁ |- Σ₂ @ lev =>
 195           Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂ @@@ lev) |- mapOptionTree drop_arg_types_as_tree Σ₂ @ lev
 196     end.
 197
 198   Definition check_hof : forall {Γ}(t:HaskType Γ ★),
 199     sumbool
 200     True
 201     (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
 202     intros.
 203     destruct (eqd_dec (take_arg_types_as_tree t) []);
 204     destruct (eqd_dec (drop_arg_types_as_tree t) t).
 205     right; auto.
 206     left; auto.
 207     left; auto.
 208     left; auto.
 209     Defined.
 210
 211   Opaque take_arg_types_as_tree.
 212   Definition skolemize_proof :
 213     forall  {h}{c},
 214       ND Rule  h c ->
 215       ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
 216     intros.
 217     eapply nd_map'; [ idtac | apply X ].
 218     clear h c X.
 219     intros.
 220
 221     refine (match X as R in Rule H C with
 222       | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _
 223       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 224       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 225       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 226       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 227       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 228       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 229       | RAbsT    Γ Δ Σ κ σ lev n       => let case_RAbsT := tt         in _
 230       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 231       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 232       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 233       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 234       | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
 235       | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
 236       | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
 237       | RVoid    _ _           l       => let case_RVoid := tt   in _
 238       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
 239       | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _
 240       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 241       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 242       end); clear X h c.
 243
 244       destruct case_RArrange.
 245         simpl.
 246         destruct l.
 247         apply nd_rule.
 248         apply SFlat.
 249         apply RArrange.
 250         apply d.
 251         apply nd_rule.
 252         apply SFlat.
 253         apply RArrange.
 254         apply ARight.
 255         apply d.
 256
 257       destruct case_RBrak.
 258         simpl.
 259         destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
 260         apply nd_rule.
 261         apply SBrak.
 262
 263       destruct case_REsc.
 264         simpl.
 265         destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
 266         apply nd_rule.
 267         apply SEsc.
 268
 269       destruct case_RNote.
 270         apply nd_rule.
 271         apply SFlat.
 272         simpl.
 273         destruct l.
 274         apply RNote.
 275         apply n.
 276         apply RNote.
 277         apply n.
 278
 279       destruct case_RLit.
 280         simpl.
 281         destruct l0.
 282         apply nd_rule.
 283         apply SFlat.
 284         apply RLit.
 285         set (check_hof (@literalType l Γ)) as hof.
 286         destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
 287         destruct a.
 288         rewrite H.
 289         rewrite H0.
 290         simpl.
 291         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ].
 292         apply nd_rule.
 293         apply SFlat.
 294         apply RLit.
 295
 296       destruct case_RVar.
 297         simpl.
 298         destruct lev.
 299         apply nd_rule; apply SFlat; apply RVar.
 300         set (check_hof σ) as hof.
 301         destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
 302         destruct a.
 303         rewrite H.
 304         rewrite H0.
 305         simpl.
 306         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
 307         apply nd_rule.
 308         apply SFlat.
 309         apply RVar.
 310
 311       destruct case_RGlobal.
 312         simpl.
 313         destruct σ.
 314         apply nd_rule; apply SFlat; apply RGlobal.
 315         set (check_hof (l wev)) as hof.
 316         destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
 317         destruct a.
 318         rewrite H.
 319         rewrite H0.
 320         simpl.
 321         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
 322         apply nd_rule.
 323         apply SFlat.
 324         apply RGlobal.
 325
 326       destruct case_RLam.
 327         destruct lev.
 328           apply nd_rule.
 329           apply SFlat.
 330           simpl.
 331           apply RLam.
 332         simpl.
 333         rewrite drop_works.
 334         apply nd_rule.
 335           apply SFlat.
 336           apply RArrange.
 337           eapply AComp.
 338           eapply AuAssoc.
 339           eapply ALeft.
 340           apply take_arrange.
 341
 342       destruct case_RCast.
 343         simpl.
 344         destruct lev.
 345         apply nd_rule.
 346         apply SFlat.
 347         apply RCast.
 348         apply γ.
 349         apply (Prelude_error "found RCast at level >0").
 350
 351       destruct case_RApp.
 352         simpl.
 353         destruct lev.
 354         apply nd_rule.
 355         apply SFlat.
 356         apply RApp.
 357         rewrite drop_works.
 358         set (check_hof tx) as hof_tx.
 359         destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
 360         destruct a.
 361         rewrite H.
 362         rewrite H0.
 363         simpl.
 364         eapply nd_comp.
 365         eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
 366         eapply nd_rule.
 367         eapply SFlat.
 368         eapply RArrange.
 369         eapply ALeft.
 370         eapply take_unarrange.
 371
 372         eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
 373         eapply nd_comp; [ apply nd_exch | idtac ].
 374         eapply nd_rule; eapply SFlat; eapply RCut.
 375
 376       destruct case_RCut.
 377         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ].
 378         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''.
 379         set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
 380         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
 381         set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.
 382         destruct (decide_tree_empty (Σ₁₂'' @@@ (h::l)));
 383           [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
 384         destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
 385         rewrite <- e.
 386         clear e.
 387         destruct s.
 388         eapply nd_comp.
 389           eapply nd_prod.
 390           eapply nd_rule.
 391           eapply SFlat.
 392           eapply RArrange.
 393           eapply AComp.
 394           eapply ALeft.
 395           eapply arrangeCancelEmptyTree with (q:=x).
 396           apply e.
 397           apply ACanR.
 398           apply nd_id.
 399         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 400         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
 401         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].
 402         apply nd_prod.
 403         apply nd_id.
 404         eapply nd_rule.
 405           eapply SFlat.
 406           eapply RArrange.
 407           eapply AComp.
 408           eapply AuAssoc.
 409           eapply ALeft.
 410           eapply AComp.
 411           eapply AuAssoc.
 412           eapply ALeft.
 413           eapply AId.
 414
 415       destruct case_RLeft.
 416         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
 417         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
 418         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
 419         set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
 420         set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
 421         destruct (decide_tree_empty (Σ' @@@ (h::l)));
 422           [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
 423         destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
 424         rewrite <- e.
 425         clear Σ'' e.
 426         destruct s.
 427         set (arrangeUnCancelEmptyTree _ _ e) as q.
 428         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ].
 429         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ].
 430         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 431         apply nd_rule.
 432         eapply SFlat.
 433         eapply RLeft.
 434
 435       destruct case_RRight.
 436         simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ].
 437         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
 438         set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
 439         set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
 440         set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
 441         destruct (decide_tree_empty (Σ' @@@ (h::l)));
 442           [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
 443         destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
 444         rewrite <- e.
 445         clear Σ'' e.
 446         destruct s.
 447         set (arrangeUnCancelEmptyTree _ _ e) as q.
 448         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ].
 449         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ].
 450         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
 451         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ].  (* yuck *)
 452         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
 453         eapply nd_rule.
 454         eapply SFlat.
 455         apply RRight.
 456
 457       destruct case_RVoid.
 458         simpl.
 459         destruct l.
 460         apply nd_rule.
 461         apply SFlat.
 462         apply RVoid.
 463         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ].
 464         apply nd_rule.
 465         apply SFlat.
 466         apply RVoid.
 467
 468       destruct case_RAppT.
 469         simpl.
 470         destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
 471         apply (Prelude_error "RAppT at depth>0").
 472
 473       destruct case_RAbsT.
 474         simpl.
 475         destruct lev; simpl.
 476           apply nd_rule.
 477           apply SFlat.
 478           apply (@RAbsT Γ Δ Σ κ σ nil n).
 479         apply (Prelude_error "RAbsT at depth>0").
 480
 481       destruct case_RAppCo.
 482         simpl.
 483         destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
 484         apply γ.
 485         apply (Prelude_error "RAppCo at depth>0").
 486
 487       destruct case_RAbsCo.
 488         simpl.
 489         destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
 490         apply (Prelude_error "RAbsCo at depth>0").
 491
 492       destruct case_RLetRec.
 493         simpl.
 494         destruct t.
 495         apply nd_rule.
 496         apply SFlat.
 497         apply (@RLetRec Γ Δ lri x y nil).
 498         destruct (decide_tree_empty (mapOptionTreeAndFlatten take_arg_types_as_tree y @@@ (h :: t)));
 499           [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ].
 500         destruct (eqd_dec y (mapOptionTree drop_arg_types_as_tree y));
 501           [ idtac | apply (Prelude_error "used LetRec on a set of bindings involving a function type") ].
 502         rewrite <- e.
 503         clear e.
 504         eapply nd_comp.
 505           eapply nd_rule.
 506           eapply SFlat.
 507           eapply RArrange.
 508           eapply ALeft.
 509           eapply AComp.
 510           eapply ARight.
 511           destruct s.
 512           apply (arrangeCancelEmptyTree _ _ e).
 513           apply ACanL.
 514         eapply nd_comp.
 515           eapply nd_rule.
 516           eapply SFlat.
 517           eapply RArrange.
 518           eapply AuAssoc.
 519         eapply nd_rule.
 520           eapply SFlat.
 521           eapply RLetRec.
 522
 523       destruct case_RCase.
 524         destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl.
 525         apply nd_rule.
 526         apply SFlat.
 527         rewrite <- mapOptionTree_compose.
 528         assert
 529           ((mapOptionTree (fun x => skolemize_judgment (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts) =
 530            (mapOptionTree (fun x => (@pcb_judg tc Γ Δ nil tbranches avars (fst x) (snd x))) alts)).
 531            admit.
 532            rewrite H.
 533         set (@RCase Γ Δ nil tc Σ avars tbranches alts) as q.
 534         apply q.
 535         Defined.
 536
 537   Transparent take_arg_types_as_tree.
 538
 539 End HaskSkolemizer.