lots of cleanup

[coq-hetmet.git] / src / HaskStrongToProof.v

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 753362e..d5e57f8 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -12,64 +12,296 @@ Require Import Coq.Init.Specif.
 Require Import HaskKinds.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskKinds.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.

-Require Import HaskWeakVars.

 Require Import HaskProof.
 
 Section HaskStrongToProof.
 
 Require Import HaskProof.
 
 Section HaskStrongToProof.
 

-(* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
- * expansion on an entire uniform proof *)
-Definition ext_left  {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
-  := @nd_map' _ _ _ _ (ext_tree_left ctx)  (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)).
-Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
-  := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)).
-
-Definition pivotContext {Γ}{Δ} a b c τ :
-  @ND _ (@URule Γ Δ)
-    [ Γ >> Δ > (a,,b),,c |- τ]
-    [ Γ >> Δ > (a,,c),,b |- τ].
-  set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q.
-  simpl in *.
-  eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ]. 
-  eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ].
-  apply q.
-  Defined.
-
-Definition copyAndPivotContext {Γ}{Δ} a b c τ :
-  @ND _ (@URule Γ Δ)
-    [ Γ >> Δ > (a,,b),,(c,,b) |- τ]
-    [ Γ >> Δ > (a,,c),,b |- τ].
-    set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q.
-    simpl in *.
-    eapply nd_comp; [ idtac | apply q ].
-    clear q.
-    eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ].
-    set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q.
-    simpl in *.
-    eapply nd_comp ; [ idtac | apply q ]. 
-    clear q.
-    apply nd_rule.
-    apply RAssoc.
-    Defined.
-
+Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
+  RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).

 
 

+Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
+  eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
+  eapply RComp; [ idtac | apply RCossa ]. 
+  eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
+  apply RAssoc.
+  Defined.

   
 Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
   
 Context {VV:Type}{eqd_vv:EqDecidable VV}.
 

-  (* maintenance of Xi *)
-  Definition dropVar (lv:list VV)(v:VV) : ??VV :=
-    if fold_left
-      (fun a b:bool => if a then true else if b then true else false)
-      (map (fun lvv => if eqd_dec lvv v then true else false) lv)
-      false
-      then None
-      else Some v.
+(* maintenance of Xi *)
+Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
+  match lv with
+    | nil     => Some v
+    | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
+  end.
+
+Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
+  match t with 
+    | T_Leaf None     => T_Leaf None
+    | T_Leaf (Some x) => T_Leaf (f x)
+    | T_Branch l r    => T_Branch (mapOptionTree' f l) (mapOptionTree' f r)
+  end.
+

   (* later: use mapOptionTreeAndFlatten *)
   Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
   (* later: use mapOptionTreeAndFlatten *)
   Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=

-    mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end).
+    mapOptionTree' (dropVar lv).
+
+Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2).
+  intros T l1.
+  induction l1; intros.
+  inversion H.
+  simpl.
+  inversion H; subst.
+  left; auto.
+  right.
+  apply IHl1.
+  apply H0.
+  Qed.
+
+Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2).
+  intros T l1.
+  induction l1; intros.
+  apply H.
+  rewrite <- app_comm_cons.
+  simpl.
+  right.
+  apply IHl1.
+  auto.
+  Qed.
+
+Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2.
+  intro T.
+  intro l1.
+  induction l1; intros.
+  split; auto.
+  apply distinct_nil.
+  simpl in H.
+  inversion H.
+  subst.
+  set (IHl1 _ H3) as H3'.
+  destruct H3'.
+  split; auto.
+  apply distinct_cons; auto.
+  intro.
+  apply H2.
+  apply In_both; auto.
+  Qed.
+
+Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B),
+  mapOptionTree' g (mapOptionTree' f t)
+  = 
+  mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t.
+  intros; induction t.
+    destruct a; auto.
+    simpl.
+    destruct (f t); reflexivity.
+    simpl.
+    rewrite <- IHt1.
+    rewrite <- IHt2.
+    reflexivity.
+    Qed.
+
+Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
+  unfold stripOutVars.
+  rewrite mapOptionTree'_compose.
+  simpl.
+  induction t.
+  destruct a0.
+  simpl.
+  induction x.
+  reflexivity.
+  simpl.
+  destruct (eqd_dec v a0).
+    destruct (eqd_dec v a); reflexivity.
+    apply IHx.
+  reflexivity.
+  simpl.
+  rewrite <- IHt1.
+  rewrite <- IHt2.
+  reflexivity.
+  Qed.
+
+Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t.
+(*
+  induction x.
+  simpl.
+  unfold stripOutVars.
+  simpl.
+  rewrite mapOptionTree'_compose.
+  induction t.
+  destruct a; try reflexivity.
+  simpl.
+  destruct (dropVar y v); reflexivity.
+  simpl.
+  rewrite IHt1.
+  rewrite IHt2.
+  reflexivity.
+  rewrite strip_lemma.
+  rewrite IHx.
+  rewrite <- strip_lemma.
+  rewrite app_comm_cons.
+  reflexivity.
+*)
+  admit.
+  Qed.
+
+Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
+  intros.
+  induction y.
+  destruct a0; try reflexivity.
+  simpl in *.
+  unfold stripOutVars.
+  simpl.
+  destruct (eqd_dec v a).
+  subst.
+  assert False.
+  apply H.
+  left; auto.
+  inversion H0.
+  auto.
+  rewrite <- IHy1 at 2.
+  rewrite <- IHy2 at 2.
+  reflexivity.
+  unfold not; intro.
+  apply H.
+  eapply In_both' in H0.
+  apply H0.
+  unfold not; intro.
+  apply H.
+  eapply In_both in H0.
+  apply H0.
+  Qed.
+
+Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
+  intros.
+  induction x.
+  reflexivity.
+  simpl.
+  destruct (eqd_dec v a).
+  subst.
+  assert False. apply H.
+  simpl; auto.
+  inversion H0.
+  apply IHx.
+  unfold not.
+  intro.
+  apply H.
+  simpl; auto.
+  Qed.
+
+Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
+  induction a; intros.
+  simpl.
+  simpl in H.
+  apply In_both'.
+  auto.
+  rewrite <- ass_app.
+  rewrite <- app_comm_cons.
+  simpl.
+  rewrite ass_app.
+  rewrite <- app_comm_cons in H.
+  inversion H.
+  left; auto.
+  right.
+  apply IHa.
+  apply H0.
+  Qed.
+
+Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
+  induction a; intros.
+  simpl in *.
+  apply distinct_app in H; auto.
+  destruct H; auto.
+  rewrite <- app_comm_cons.
+  apply distinct_cons.
+  rewrite <- ass_app in H.
+  rewrite <- app_comm_cons in H.
+  inversion H.
+  subst.
+  intro q.
+  apply H2.
+  rewrite ass_app.
+  apply in3.
+  auto.
+  apply IHa.
+  rewrite <- ass_app.
+  rewrite <- ass_app in H.
+  rewrite <- app_comm_cons in H.
+  inversion H.
+  subst.
+  auto.
+  Qed.
+
+Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
+  induction x; intros.
+  simpl in H.
+  unfold stripOutVars.
+  simpl.
+  induction y; try destruct a; auto.
+  simpl.
+  rewrite IHy1.
+  rewrite IHy2.
+  reflexivity.
+  simpl in H.
+  apply distinct_app in H; destruct H; auto.
+  apply distinct_app in H; destruct H; auto.
+  rewrite <- app_comm_cons in H.
+  inversion H; subst.
+  set (IHx H3) as qq.
+  rewrite strip_lemma.
+  rewrite IHx.
+  apply strip_distinct.
+  unfold not; intros.
+  apply H2.
+  apply In_both'.
+  auto.
+  auto.
+  Qed.
+
+Lemma updating_stripped_tree_is_inert'
+  {Γ} lev
+  (ξ:VV -> LeveledHaskType Γ ★)
+  lv tree2 :
+    mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
+  = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
+  induction tree2.
+  destruct a.
+  simpl.
+  induction lv.
+  reflexivity.
+  simpl.
+  destruct a.
+  simpl.
+  set (eqd_dec v v0) as q.
+  destruct q.
+  auto.
+  set (dropVar (map (@fst _ _) lv) v) as b in *.
+  destruct b.
+  inversion IHlv.
+  admit.
+  auto.
+  reflexivity.
+  simpl.
+  unfold stripOutVars in *.
+  rewrite <- IHtree2_1.
+  rewrite <- IHtree2_2.
+  reflexivity.
+  Qed.
+
+Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)),
+  distinct (map (@fst _ _) (leaves varstypes)) ->
+  mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
+  mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
+  admit.
+  Qed.
+
+
+
+

 
 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
   match exp as E in Expr Γ Δ ξ τ with
 
 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
   match exp as E in Expr Γ Δ ξ τ with

+  | EGlobal  Γ Δ ξ _ _                            => []

   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)

@@ -89,60 +321,49 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ?
    in     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
   | ECase    Γ Δ ξ l tc tbranches atypes e' alts =>
     ((fix varsfromalts (alts:
    in     stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
   | ECase    Γ Δ ξ l tc tbranches atypes e' alts =>
     ((fix varsfromalts (alts:

-               Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
+               Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+                            & Expr (sac_Γ sac Γ)
+                                   (sac_Δ sac Γ atypes (weakCK'' Δ))

                                    (scbwv_ξ scb ξ l)
                                    (scbwv_ξ scb ξ l)

-                                   (weakLT' (tbranches@@l)) }
+                                   (weakLT' (tbranches@@l)) } }

       ): Tree ??VV :=
       match alts with
         | T_Leaf None     => []
       ): Tree ??VV :=
       match alts with
         | T_Leaf None     => []

-        | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h))
+        | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))

         | T_Branch b1 b2  => (varsfromalts b1),,(varsfromalts b2)
       end) alts),,(expr2antecedent e')
 end
 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
 match elrb with
   | ELR_nil    Γ Δ ξ lev  => []
         | T_Branch b1 b2  => (varsfromalts b1),,(varsfromalts b2)
       end) alts),,(expr2antecedent e')
 end
 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
 match elrb with
   | ELR_nil    Γ Δ ξ lev  => []

-  | ELR_leaf   Γ Δ ξ lev v e => expr2antecedent e
+  | ELR_leaf   Γ Δ ξ lev v t e => expr2antecedent e

   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
 end.
 
 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
   | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
 end.
 
 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}

-  (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
+(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+                            & Expr (sac_Γ sac Γ)
+                                   (sac_Δ sac Γ atypes (weakCK'' Δ))

                                    (scbwv_ξ scb ξ l)
                                    (scbwv_ξ scb ξ l)

-                                   (weakLT' (tbranches@@l)) })
-  : ProofCaseBranch tc Γ Δ l tbranches atypes.
+                                   (weakLT' (tbranches@@l)) } })
+  : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
+  destruct alt.
+  exists x.

   exact
   exact

-    {| pcb_scb := projT1 alt
-     ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt)))
+    {| pcb_freevars := mapOptionTree ξ
+      (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
+        (expr2antecedent (projT2 s)))

      |}.
      Defined.
 
      |}.
      Defined.
 

-Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) :=
-  match elrb with
-  | ELR_nil    Γ Δ ξ lev  => []
-  | ELR_leaf   Γ Δ ξ  lev  v e => [ξ v]
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
-  end.

 
 

-Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
+Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=

   match elrb with
   | ELR_nil    Γ Δ ξ lev  => []
   match elrb with
   | ELR_nil    Γ Δ ξ lev  => []

-  | ELR_leaf   Γ Δ ξ  lev  v e => [v]
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
-  end.
-
-Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):=
-  match elrb with
-  | ELR_nil    Γ Δ ξ lev  => []
-  | ELR_leaf   Γ Δ ξ  lev  v e => [(v, ξ v)]
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
+  | ELR_leaf   Γ Δ ξ  lev  v t e => [t]
+  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)

   end.
 
   end.
 

-

 Lemma stripping_nothing_is_inert
   {Γ:TypeEnv}
   (ξ:VV -> LeveledHaskType Γ ★)
 Lemma stripping_nothing_is_inert
   {Γ:TypeEnv}
   (ξ:VV -> LeveledHaskType Γ ★)

@@ -154,57 +375,52 @@ Lemma stripping_nothing_is_inert
     fold stripOutVars.
     simpl.
     fold (stripOutVars nil).
     fold stripOutVars.
     simpl.
     fold (stripOutVars nil).

-    rewrite IHtree1.
-    rewrite IHtree2.
+    rewrite <- IHtree1 at 2.
+    rewrite <- IHtree2 at 2.

     reflexivity.
     Qed.
 
     reflexivity.
     Qed.
 

-
-
-Definition arrangeContext 
+Definition arrangeContext

      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
      ctx    (* initial context *)
      (Γ:TypeEnv)(Δ:CoercionEnv Γ)
      v      (* variable to be pivoted, if found *)
      ctx    (* initial context *)

-     τ      (* type of succedent *)

      (ξ:VV -> LeveledHaskType Γ ★)
      :
  
     (* a proof concluding in a context where that variable does not appear *)
      (ξ:VV -> LeveledHaskType Γ ★)
      :
  
     (* a proof concluding in a context where that variable does not appear *)

-    sum (ND (@URule Γ Δ)
-          [Γ >> Δ > mapOptionTree ξ                        ctx                        |- τ]
-          [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   |- τ])
+     sum (Arrange
+          (mapOptionTree ξ                        ctx                        )
+          (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[]                   ))

    
     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
    
     (* or a proof concluding in a context where that variable appears exactly once in the left branch *)

-        (ND (@URule Γ Δ)
-          [Γ >> Δ > mapOptionTree ξ                         ctx                       |- τ]
-          [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                |- τ]).
+        (Arrange
+          (mapOptionTree ξ                         ctx                       )
+          (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])                )).

 
 

-  induction ctx; simpl in *.
+  induction ctx.

   
   

-    refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *.
+    refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).

   
         (* nonempty leaf *)
         destruct case_Some.
           unfold stripOutVars in *; simpl.
           unfold dropVar.
           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
   
         (* nonempty leaf *)
         destruct case_Some.
           unfold stripOutVars in *; simpl.
           unfold dropVar.
           unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.

-          destruct (eqd_dec v v'); simpl in *.

 
 

+          destruct (eqd_dec v' v); subst.
+          

             (* where the leaf is v *)
             apply inr.
               subst.
             (* where the leaf is v *)
             apply inr.
               subst.

-              apply nd_rule.

               apply RuCanL.
 
             (* where the leaf is NOT v *)
             apply inl.
               apply RuCanL.
 
             (* where the leaf is NOT v *)
             apply inl.

-              apply nd_rule.

               apply RuCanR.
   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.
               apply RuCanR.
   
         (* empty leaf *)
         destruct case_None.
           apply inl; simpl in *.

-          apply nd_rule.

           apply RuCanR.
   
       (* branch *)
           apply RuCanR.
   
       (* branch *)

@@ -224,86 +440,90 @@ Definition arrangeContext
 
     destruct case_Neither.
       apply inl.
 
     destruct case_Neither.
       apply inl.

-      eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ].
-        exact (nd_comp
+      eapply RComp; [idtac | apply RuCanR ].
+        exact (RComp

           (* order will not matter because these are central as morphisms *)
           (* order will not matter because these are central as morphisms *)

-          (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _))))
-          (ext_left  _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))).
+          (RRight _ (RComp lpf (RCanR _)))
+          (RLeft  _ (RComp rpf (RCanR _)))).

 
 
     destruct case_Right.
       apply inr.
       fold (stripOutVars (v::nil)).
 
 
     destruct case_Right.
       apply inr.
       fold (stripOutVars (v::nil)).

-      set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q.
+      set (RRight (mapOptionTree ξ ctx2)  (RComp lpf ((RCanR _)))) as q.

       simpl in *.
       simpl in *.

-      eapply nd_comp.
+      eapply RComp.

       apply q.
       clear q.
       clear lpf.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       apply q.
       clear q.
       clear lpf.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.

-      eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ].
-      set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ]
-                                                            [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v])  |- τ]) as qq.
-      apply qq.
-      clear qq.
+      eapply RComp; [ idtac | apply RAssoc ].
+      apply RLeft.

       apply rpf.
 
     destruct case_Left.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).
       apply rpf.
 
     destruct case_Left.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).

-      eapply nd_comp; [ idtac | eapply pivotContext ].
-      set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'.
-      set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq.
+      eapply RComp; [ idtac | eapply pivotContext ].
+      set (RComp rpf (RCanR _ )) as rpf'.
+      set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.

       simpl in *.
       simpl in *.

-      eapply nd_comp; [ idtac | apply qq ].
+      eapply RComp; [ idtac | apply qq ].

       clear qq rpf' rpf.
       clear qq rpf' rpf.

-      set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q.
-      apply q.
-      clear q.
+      apply (RRight (mapOptionTree ξ ctx2)).

       apply lpf.
 
     destruct case_Both.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).
       apply lpf.
 
     destruct case_Both.
       apply inr.
       unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
       fold (stripOutVars (v::nil)).

-      eapply nd_comp; [ idtac | eapply copyAndPivotContext ].
-        exact (nd_comp
-          (* order will not matter because these are central as morphisms *)
-          (ext_right _ _ _ lpf)
-          (ext_left  _ _ _ rpf)).
+      eapply RComp; [ idtac | eapply copyAndPivotContext ].
+        (* order will not matter because these are central as morphisms *)
+        exact (RComp (RRight _ lpf) (RLeft _ rpf)).

 
     Defined.
 
 (* same as before, but use RWeak if necessary *)
 
     Defined.
 
 (* same as before, but use RWeak if necessary *)

-Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ : 
-       ND (@URule Γ Δ)
-          [Γ >> Δ>mapOptionTree ξ                        ctx                |- τ]
-          [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        |- τ].
-  set (arrangeContext Γ Δ v ctx τ ξ) as q.
+Definition arrangeContextAndWeaken  
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     ctx    (* initial context *)
+     (ξ:VV -> LeveledHaskType Γ ★) :
+       Arrange
+          (mapOptionTree ξ                        ctx                )
+          (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v])        ).
+  set (arrangeContext Γ Δ v ctx ξ) as q.

   destruct q; auto.
   destruct q; auto.

-  eapply nd_comp; [ apply n | idtac ].
-  clear n.
-  refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
+  eapply RComp; [ apply a | idtac ].
+  refine (RLeft _ (RWeak _)).

   Defined.
 
   Defined.
 

-Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, 
-  ND (@URule Γ Δ)
-    [Γ >> Δ>(mapOptionTree ξ ctx)                                       |-  z]
-    [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |-  z].
+Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
+  admit.
+  Qed.
+
+Definition arrangeContextAndWeaken''
+     (Γ:TypeEnv)(Δ:CoercionEnv Γ)
+     v      (* variable to be pivoted, if found *)
+     (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
+  distinct (leaves v) ->
+  Arrange
+    ((mapOptionTree ξ ctx)                                       )
+    ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).

 
 

-  induction v.
+  induction v; intros.

     destruct a.
     unfold mapOptionTree in *.
     simpl in *.
     fold (mapOptionTree ξ) in *.
     intros.
     apply arrangeContextAndWeaken.
     destruct a.
     unfold mapOptionTree in *.
     simpl in *.
     fold (mapOptionTree ξ) in *.
     intros.
     apply arrangeContextAndWeaken.

+    apply Δ.

 
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.
 
   unfold mapOptionTree; simpl in *.
     intros.
     rewrite (@stripping_nothing_is_inert Γ); auto.

-    apply nd_rule.

     apply RuCanR.
     intros.
     unfold mapOptionTree in *.
     apply RuCanR.
     intros.
     unfold mapOptionTree in *.

@@ -311,7 +531,7 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     fold (mapOptionTree ξ) in *.
     set (mapOptionTree ξ) as X in *.
 
     fold (mapOptionTree ξ) in *.
     set (mapOptionTree ξ) as X in *.
 

-    set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'.
+    set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.

     unfold stripOutVars in IHv2'.
     simpl in IHv2'.
     fold (stripOutVars (leaves v2)) in IHv2'.
     unfold stripOutVars in IHv2'.
     simpl in IHv2'.
     fold (stripOutVars (leaves v2)) in IHv2'.

@@ -321,230 +541,171 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
     simpl in IHv2'.
     fold (mapOptionTree ξ) in IHv2'.
     fold X in IHv2'.
     simpl in IHv2'.
     fold (mapOptionTree ξ) in IHv2'.
     fold X in IHv2'.

-    set (nd_comp (IHv1 _ _) IHv2') as qq.
-    eapply nd_comp.
+    set (distinct_app _ _ _ H) as H'.
+    destruct H' as [H1 H2].
+    set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
+    eapply RComp.

       apply qq.
       clear qq IHv2' IHv2 IHv1.
       apply qq.
       clear qq IHv2' IHv2 IHv1.

-        
-      assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)).
-        admit.
-        rewrite H.
-        clear H.
-
-      (* FIXME: this only works because the variables are all distinct, but I need to prove that *)
-      assert ((stripOutVars (leaves v2) v1) = v1).
-        admit.
-        rewrite H.
-        clear H.
-
-        apply nd_rule.
+      rewrite strip_twice_lemma.
+
+      rewrite (strip_distinct' v1 (leaves v2)).

         apply RCossa.
         apply RCossa.

+        apply cheat.
+        auto.

     Defined.
 
     Defined.
 

-Definition update_ξ'' {Γ} ξ tree lev :=
-(update_ξ ξ
-                  (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@  lev ⟩)
-                     (leaves tree))).
-
-Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev :
-      mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree)
+Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
+      mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)

     = mapOptionTree ξ (stripOutVars (v :: nil) tree).
     = mapOptionTree ξ (stripOutVars (v :: nil) tree).

-  induction tree; simpl in *; try reflexivity; auto.
-
-  unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *.
-  destruct a; simpl; try reflexivity.
-  unfold update_ξ.
-  simpl.
-  unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
-  unfold update_ξ.
-  unfold dropVar.
+  set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
+  rewrite p.

   simpl.
   simpl.

-  set (eqd_dec v v0) as q.
-  assert (q=eqd_dec v v0).
-    reflexivity.
-  destruct q.
-  reflexivity.
-  rewrite <- H.
-  reflexivity.
-  auto.
-  unfold mapOptionTree.
-  unfold mapOptionTree in IHtree1.
-  unfold mapOptionTree in IHtree2.
-  simpl in *.
-  simpl in IHtree1.
-  fold (stripOutVars (v::nil)).
-  rewrite <- IHtree1.
-  rewrite <- IHtree2.

   reflexivity.
   Qed.
 
   reflexivity.
   Qed.
 

-
-
-Lemma updating_stripped_tree_is_inert'
-  {Γ} lev
-  (ξ:VV -> LeveledHaskType Γ ★)
-  tree tree2 :
-    mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
-  = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2).
-admit.
-  Qed.
-
-Lemma updating_stripped_tree_is_inert''
-  {Γ}
-  (ξ:VV -> LeveledHaskType Γ ★)
-  v tree lev :
-    mapOptionTree   (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree)
-  = mapOptionTree ξ (stripOutVars  (map (@fst _ _) v) tree).
-admit.
-  Qed.
-
-(*
-Lemma updating_stripped_tree_is_inert'''
-  {Γ}
-  (ξ:VV -> LeveledHaskType Γ)
-{T}
-  (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree
-:
-    mapOptionTree   (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree)
-  = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree).
-admit.
-  Qed.
-*)
-
-(* IDEA: use multi-conclusion proofs instead *)
+(* TODO: use multi-conclusion proofs instead *)

 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := 
   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := 
   | lrsp_nil  : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)

-  | lrsp_leaf : forall v  e,
-    (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) ->
-    LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e)
+  | lrsp_leaf : forall v t e ,
+    (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
+    LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)

   | lrsp_cons : forall t1 t2 b1 b2,
     LetRecSubproofs Γ Δ ξ lev t1 b1 ->
     LetRecSubproofs Γ Δ ξ lev t2 b2 ->
     LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
 
   | lrsp_cons : forall t1 t2 b1 b2,
     LetRecSubproofs Γ Δ ξ lev t1 b1 ->
     LetRecSubproofs Γ Δ ξ lev t2 b2 ->
     LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
 

-Lemma cheat9 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
-
-  eLetRecTypes branches =
-    mapOptionTree  (update_ξ'' ξ tree lev)
-    (mapOptionTree (@fst _ _) tree).
-  intros.
-  induction branches.
-  reflexivity.
-  simpl.
-  unfold update_ξ.
-  unfold mapOptionTree; simpl.
-admit.
-admit.
-  Qed.
-
-Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
-    : LetRecSubproofs Γ Δ ξ lev tree branches ->
-    ND Rule []
-    [ Γ > Δ >
-      mapOptionTree ξ (eLetRecContext branches)
-      |-
-  eLetRecTypes branches
-    ].
-  intro X.
-  induction X; intros; simpl in *.
+Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
+  LetRecSubproofs Γ Δ ξ lev tree branches ->
+    ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
+      |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
+  intro X; induction X; intros; simpl in *.

     apply nd_rule.
       apply REmptyGroup.
     apply nd_rule.
       apply REmptyGroup.

-    unfold mapOptionTree.
-      simpl.
-admit.
-(*      apply n.*)
+    set (ξ v) as q in *.
+      destruct q.
+      simpl in *.
+      apply n.

     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
   Defined.
 
     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
   Defined.
 

-
-Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev,
-  mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
-admit.
-  Qed.
-
-
-

 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
     forall branches body,
 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
     forall branches body,

-    ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] -> 
-    LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches ->
+    distinct (leaves (mapOptionTree (@fst _ _) tree)) ->
+    ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> 
+    LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->

     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
 
   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
     ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
 
   (* NOTE: how we interpret stuff here affects the order-of-side-effects *)

-  simpl.

   intro branches.
   intro body.
   intro branches.
   intro body.

+  intro disti.

   intro pf.
   intro lrsp.
   intro pf.
   intro lrsp.

-  set ((update_ξ ξ
-           (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@  lev ⟩)
-              (leaves tree)))) as ξ' in *.
+
+  rewrite mapleaves in disti.
+  set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma.
+    rewrite <- mapOptionTree_compose in ξlemma.
+
+  set ((update_ξ ξ lev (leaves tree))) as ξ' in *.

   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
   set (mapOptionTree (@fst _ _) tree) as pctx.
   set (mapOptionTree ξ' pctx) as passback.
   set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
   set (mapOptionTree (@fst _ _) tree) as pctx.
   set (mapOptionTree ξ' pctx) as passback.

-  set (fun a b => @RLetRec Γ Δ a b passback) as z.
+  set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.

   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 

-  set (@arrangeContextAndWeaken''  Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
+  set (@arrangeContextAndWeaken''  Γ Δ  pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'.

   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.
   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.

-  eapply UND_to_ND in q'.
+  rewrite <- mapleaves in disti.
+  set (q' disti) as q''.

 
   unfold ξ' in *.
 
   unfold ξ' in *.

-  set (@updating_stripped_tree_is_inert') as zz.
-  unfold update_ξ'' in *.
-  rewrite zz in q'.
+  set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
+  rewrite <- mapleaves in zz.
+  rewrite zz in q''.

   clear zz.
   clear ξ'.
   clear zz.
   clear ξ'.

-  simpl in q'.
-
-  eapply nd_comp; [ idtac | apply q' ].
+  Opaque stripOutVars.
+  simpl.
+  rewrite <- mapOptionTree_compose in q''.
+  rewrite <- ξlemma.
+  eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ].

   clear q'.
   clear q'.

-  unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)).
-
+  clear q''.

   simpl.
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
   simpl.
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.

-

     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.
     eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     apply nd_prod; auto.

-    rewrite cheat9 in q.
-    set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
-    unfold update_ξ'' in *.
-    rewrite <- zz in q.
+    rewrite ξlemma.

     apply q.
     apply q.

-  Defined.
+    Defined.

 
 

-(*
-Lemma update_ξ_and_reapply : forall Γ ξ {T}(idx:Tree ??T)(types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx),
-  unshape types = mapOptionTree (update_ξ''' ξ types vars) (unshape vars).
-admit.
+Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
+  forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
+    forall l ξ,
+      vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
+      vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
+  intros.
+  unfold scbwv_ξ.
+  unfold scbwv_varstypes.
+  set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
+    (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
+    ) as q.
+  rewrite <- mapleaves' in q.
+  rewrite <- mapleaves' in q.
+  rewrite <- mapleaves' in q.
+  rewrite <- mapleaves' in q.
+  set (fun z => unleaves_injective _ _ _ (q z)) as q'.
+  rewrite vec2list_map_list2vec in q'.
+  rewrite fst_zip in q'.
+  rewrite vec2list_map_list2vec in q'.
+  rewrite vec2list_map_list2vec in q'.
+  rewrite snd_zip in q'.
+  rewrite leaves_unleaves in q'.
+  rewrite vec2list_map_list2vec in q'.
+  rewrite vec2list_map_list2vec in q'.
+  apply q'.
+  rewrite fst_zip.
+  apply scbwv_exprvars_distinct.

   Qed.
   Qed.

-*)

 
 

-Lemma cheat0 : forall Γ Δ ξ l tc tbranches atypes e alts',
-mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
-= 
-(*
-((mapOptionTreeAndFlatten
-(fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
-                  (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
-*)
-((mapOptionTreeAndFlatten pcb_freevars
-           (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ  (expr2antecedent e)).
-admit.
-Defined.

 
 

-Lemma cheat1 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
-  admit.
-  Defined.
-Lemma cheat2 : forall {A}(t:list A), leaves (unleaves t) = t.
-admit.
-Defined.
+Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
+   (alts':Tree
+            ??{sac : StrongAltCon &
+              {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
+              Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
+                (scbwv_ξ scb ξ l) (weakLT' (tbranches @@  l))}}),
+
+      (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
+        (mapOptionTree mkProofCaseBranch alts'))
+    ,,
+    mapOptionTree ξ  (expr2antecedent e) =
+  mapOptionTree ξ
+        (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
+  intros.
+  simpl.
+  Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
+  hack.
+  induction alts'.
+  destruct a; simpl.
+  destruct s; simpl.
+  unfold mkProofCaseBranch.
+  reflexivity.
+  reflexivity.
+  simpl.
+  rewrite IHalts'1.
+  rewrite IHalts'2.
+  reflexivity.
+  rewrite H.
+  reflexivity.
+  Qed.

 
 Definition expr2proof  :
   forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
 
 Definition expr2proof  :
   forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),

@@ -553,54 +714,62 @@ Definition expr2proof  :
   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
     match exp as E in Expr Γ Δ ξ τ with
   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
     match exp as E in Expr Γ Δ ξ τ with

+    | EGlobal  Γ Δ ξ t wev                          => let case_EGlobal := tt in _

     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in 
     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in 

-      let e1' := expr2proof _ _ _ _ e1 in
-      let e2' := expr2proof _ _ _ _ e2 in _
-    | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in 
-      let e' := expr2proof _ _ _ _ e in _
+                                                        (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
+    | ELam     Γ Δ ξ t1 t2 lev v    e               => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)

     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in 
     | ELet     Γ Δ ξ tv t      v lev ev ebody       => let case_ELet := tt in 

-      let pf_let := (expr2proof _ _ _ _ ev) in
-      let pf_body := (expr2proof _ _ _ _ ebody) in _
+                                                       (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) 

     | ELetRec  Γ Δ ξ lev t tree branches ebody      =>
     | ELetRec  Γ Δ ξ lev t tree branches ebody      =>

-      let e' := expr2proof _ _ _ _ ebody in 
-      let ξ' := update_ξ'' ξ tree lev in
-      let subproofs := ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
+      let ξ' := update_ξ ξ lev (leaves tree) in
+      let case_ELetRec := tt in  (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) 
+        ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))

         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
         (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
         : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
         match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with

-  | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
-  | ELR_leaf   Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
-  | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
+          | ELR_nil    Γ Δ ξ lev  => lrsp_nil _ _ _ _
+          | ELR_leaf   Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
+          | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)

         end
         end

-        ) _ _ _ _ tree branches) in
-      let case_ELetRec := tt in  _
-    | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in let e' := expr2proof _ _ _ _ e in _
-    | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in let e' := expr2proof _ _ _ _ e in _
-    | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in let e' := expr2proof _ _ _ _ e in _
-    | ENote    Γ Δ ξ t n e                          => let case_ENote   := tt in let e' := expr2proof _ _ _ _ e in _
-    | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in let e' := expr2proof _ _ _ _ e in _
-    | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in let e' := expr2proof _ _ _ _ e in _
-    | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in let e' := expr2proof _ _ _ _ e in _
-    | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in let e' := expr2proof _ _ _ _ e in _
+        ) _ _ _ _ tree branches)
+    | EEsc     Γ Δ ξ ec t lev e                     => let case_EEsc    := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+    | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+    | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+    | ENote    Γ Δ ξ t n e                          => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+    | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+    | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+    | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)
+    | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ e)

     | ECase    Γ Δ ξ l tc tbranches atypes e alts' => 
       let dcsp :=
         ((fix mkdcsp (alts:
     | ECase    Γ Δ ξ l tc tbranches atypes e alts' => 
       let dcsp :=
         ((fix mkdcsp (alts:

-               Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
-                            & Expr (sac_Γ scb Γ)
-                                   (sac_Δ scb Γ atypes (weakCK'' Δ))
+               Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
+                            & Expr (sac_Γ sac Γ)
+                                   (sac_Δ sac Γ atypes (weakCK'' Δ))

                                    (scbwv_ξ scb ξ l)
                                    (scbwv_ξ scb ξ l)

-                                   (weakLT' (tbranches@@l)) })
-          : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
-        match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
-          | T_Leaf None       => let case_nil := tt in _
-          | T_Leaf (Some x)   => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
-          | T_Branch b1 b2   => let case_branch := tt in _
+                                   (weakLT' (tbranches@@l)) } })
+          : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
+        match alts as ALTS return ND Rule [] 
+          (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
+          | T_Leaf None      => let case_nil := tt in _
+          | T_Branch b1 b2   => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
+          | T_Leaf (Some x)  =>
+            match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
+            existT sac (existT scbx ex) =>
+            (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
+        end

         end) alts')
         in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
     end
         end) alts')
         in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
     end

-); clear exp ξ' τ' Γ' Δ'.
+  ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
+
+    destruct case_EGlobal.
+      apply nd_rule.
+      simpl.
+      destruct t as [t lev].
+      apply (RGlobal _ _ _ _ wev).

 
     destruct case_EVar.
       apply nd_rule.
 
     destruct case_EVar.
       apply nd_rule.

@@ -617,20 +786,21 @@ Definition expr2proof  :
       eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; auto.
       eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; auto.

+      apply e1'.
+      apply e2'.

 
     destruct case_ELam; intros.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
 
     destruct case_ELam; intros.
       unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
       eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].

-      set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
-      set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
-        apply UND_to_ND in pfx.
-        unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
+      set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
+      set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
+        eapply RArrange in pfx.
+        unfold mapOptionTree in pfx; simpl in pfx.

         unfold ξ' in pfx.
         unfold ξ' in pfx.

-        fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.

         rewrite updating_stripped_tree_is_inert in pfx.
         unfold update_ξ in pfx.
         destruct (eqd_dec v v).
         rewrite updating_stripped_tree_is_inert in pfx.
         unfold update_ξ in pfx.
         destruct (eqd_dec v v).

-        eapply nd_comp; [ idtac | apply pfx ].
+        eapply nd_comp; [ idtac | apply (nd_rule pfx) ].

         clear pfx.
         apply e'.
         assert False.
         clear pfx.
         apply e'.
         assert False.

@@ -641,14 +811,15 @@ Definition expr2proof  :
     destruct case_ELet; intros; simpl in *.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
     destruct case_ELet; intros; simpl in *.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].

-      apply nd_prod; [ idtac | apply pf_let].
-      clear pf_let.
-      eapply nd_comp; [ apply pf_body | idtac ].
-      clear pf_body.
+      apply nd_prod.
+        apply pf_let.
+        clear pf_let.
+        eapply nd_comp; [ apply pf_body | idtac ].
+        clear pf_body.

       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).

-      set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
-      set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
+      set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
+      set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.

       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
       unfold ξ' in n.
       rewrite updating_stripped_tree_is_inert in n.
       unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
       unfold ξ' in n.
       rewrite updating_stripped_tree_is_inert in n.

@@ -656,8 +827,8 @@ Definition expr2proof  :
       destruct (eqd_dec lev lev).
       unfold ξ'.
       unfold update_ξ.
       destruct (eqd_dec lev lev).
       unfold ξ'.
       unfold update_ξ.

-      apply UND_to_ND in n.
-      apply n.
+      eapply RArrange in n.
+      apply (nd_rule n).

       assert False. apply n0; auto. inversion H.
 
     destruct case_EEsc.
       assert False. apply n0; auto. inversion H.
 
     destruct case_EEsc.

@@ -674,6 +845,7 @@ Definition expr2proof  :
       auto.
 
     destruct case_ENote.
       auto.
 
     destruct case_ENote.

+      destruct t.

       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
       apply e'.
       auto.
       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
       apply e'.
       auto.

@@ -683,121 +855,85 @@ Definition expr2proof  :
       apply e'.
       auto.
 
       apply e'.
       auto.
 

+    destruct case_ECoLam; simpl in *; intros.
+      eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
+      apply e'.
+

     destruct case_ECoApp; simpl in *; intros.
       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
       apply e'.
       auto.
 
     destruct case_ECoApp; simpl in *; intros.
       eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
       apply e'.
       auto.
 

+    destruct case_ETyLam; intros.
+      eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
+      unfold mapOptionTree in e'.
+      rewrite mapOptionTree_compose in e'.
+      unfold mapOptionTree.
+      apply e'.
+

     destruct case_leaf.
     destruct case_leaf.

-      unfold pcb_judg.
+      clear o x alts alts' e.
+      eapply nd_comp; [ apply e' | idtac ].
+      clear e'.
+      apply nd_rule.
+      apply RArrange.

       simpl.
       simpl.

-      repeat rewrite <- mapOptionTree_compose in *.
-      set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
-        (unleaves (vec2list (scbwv_exprvars (projT1 x))))
-      (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
-        _ _
-      ))) as q.
-
-rewrite cheat2 in q.
-rewrite cheat1.
-unfold weakCK'' in q.
-simpl in q.
-admit.
-(*
-replace (mapOptionTree ((@weakLT' Γ (tyConKind tc) _) ○ ξ)
-        (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
-           (expr2antecedent (projT2 x))))
-with (mapOptionTree (scbwv_ξ (projT1 x) ξ l)
-              (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
-                 (expr2antecedent (projT2 x)))).
-rewrite <- cheat1 in q.
-rewrite vec2list_map_list2vec in q.
-unfold mapOptionTree.
-fold (@mapOptionTree (HaskType (app (tyConKind tc) Γ) ★)
- (LeveledHaskType (app (tyConKind tc) Γ) ★) (fun t' => t' @@ weakL' l)).
-admit.
-*)
-admit.
-
-(*
-assert (
-
-unleaves (vec2list (vec_map (scbwv_ξ (projT1 x) ξ l) (scbwv_exprvars (projT1 x))))
-=
-unleaves (vec2list (sac_types (projT1 x) Γ atypes)) @@@ weakL'(κ:=tyConKind tc) l).
-admit.
-Set Printing Implicit.
-idtac.
-rewrite <- H.
-
-      assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))).
-      apply update_ξ_and_reapply.
-      rewrite H.
-      simpl in q.
-      unfold mapOptionTree in q; simpl in q.
-      set (@updating_stripped_tree_is_inert''') as u.
-      unfold mapOptionTree in u.
-      rewrite u in q.
-      clear u H.
-      unfold weakenX' in *.
-      admit.
-      unfold mapOptionTree in *.
-      replace
-        (@weakenT' _ (sac_ekinds alt) (coreTypeToType φ tbranches0))
-        with
-        (coreTypeToType (updatePhi φ (sac_evars alt)) tbranches0).
+      rewrite mapleaves'.
+      simpl.
+      rewrite <- mapOptionTree_compose.
+      unfold scbwv_ξ.
+      rewrite <- mapleaves'.
+      rewrite vec2list_map_list2vec.
+      unfold sac_Γ.      
+      rewrite <- (scbwv_coherent scbx l ξ).
+      rewrite <- vec2list_map_list2vec.
+      rewrite mapleaves'.
+      set (@arrangeContextAndWeaken'') as q.
+      unfold scbwv_ξ.
+      set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
+      unfold scbwv_varstypes in z.
+      rewrite vec2list_map_list2vec in z.
+      rewrite fst_zip in z.
+      rewrite <- z.
+      clear z.
+      replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
+        (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).

       apply q.
       apply q.

-      apply cheat.
-*)
+      apply (sac_Δ sac Γ atypes (weakCK'' Δ)).
+      rewrite leaves_unleaves.
+      apply (scbwv_exprvars_distinct scbx).
+      rewrite leaves_unleaves.
+      reflexivity.
+
+    destruct case_nil.
+      apply nd_id0.

 
     destruct case_branch.
       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.
 
     destruct case_branch.
       simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.

-      apply (mkdcsp b1).
-      apply (mkdcsp b2).
+      apply b1'.
+      apply b2'.

 
     destruct case_ECase.
 
     destruct case_ECase.

-      rewrite cheat0.
+    set (@RCase Γ Δ l tc) as q.
+      rewrite <- case_lemma.

       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
       rewrite <- mapOptionTree_compose.
       apply dcsp.
       apply e'.
 
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
       eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
       rewrite <- mapOptionTree_compose.
       apply dcsp.
       apply e'.
 

-    destruct case_ELetRec; simpl in *; intros.
-      set (@letRecSubproofsToND') as q.
-      simpl in q.
-      apply q.
-      clear q.
+    destruct case_ELetRec; intros.
+      unfold ξ'0 in *.
+      clear ξ'0.
+      unfold ξ'1 in *.
+      clear ξ'1.
+      apply letRecSubproofsToND'.
+      admit.

       apply e'.
       apply subproofs.
 
       apply e'.
       apply subproofs.
 

-    (*
-    destruct case_ECoLam; simpl in *; intros.
-      eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
-      apply e'.
-
-    destruct case_ETyLam; intros.
-      eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
-      unfold mapOptionTree in e'.
-      rewrite mapOptionTree_compose in e'.
-      unfold mapOptionTree.
-      apply e'.
-     *)
-  Admitted.
+  Defined.

 
 End HaskStrongToProof.
 
 
 End HaskStrongToProof.
 

-(*
-
-(* Figure 7, production "decl"; actually not used in this formalization *)
-Inductive Decl :=.
-| DeclDataType     : forall tc:TyCon,      (forall dc:DataCon tc, DataConDecl dc)      -> Decl
-| DeclTypeFunction : forall n t l,         TypeFunctionDecl n t l                      -> Decl
-| DeclAxiom        : forall n ccon vk TV,  @AxiomDecl        n ccon vk  TV             -> Decl.
-
-(* Figure 1, production "pgm" *)
-Inductive Pgm Γ Δ :=
-  mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.
-*)
-