+ Definition mkBrak {Γ}{Δ}(j:Tree ??(UJudg Γ Δ)) v h
+ : ND Rule
+ (mapOptionTree (fun j => @UJudg2judg Γ Δ (brakifyu v j)) h)
+ (mapOptionTree (@UJudg2judg Γ Δ ) h).
+ admit.
+ Defined.
+
+ (* any proof in organized form can be "dis-organized" *)
+ Definition unOrgR b n Γ Δ : forall h c, OrgR b n Γ Δ h c ->
+ ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c).
+
+ intros.
+
+ induction X.
+ apply nd_rule.
+ destruct p.
+ apply x.
+
+ apply n0.
+
+ rewrite <- mapOptionTree_compose.
+ rewrite <- mapOptionTree_compose.
+ eapply nd_comp.
+ apply (mkBrak h).
+ eapply nd_comp; [ idtac | apply (mkEsc c) ].
+ apply IHX.
+ Defined.
+
+ Definition unOrgND b n Γ Δ h c :
+ ND (OrgR b n Γ Δ) h c -> ND Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c)
+ := nd_map' (@UJudg2judg Γ Δ) (unOrgR b n Γ Δ).
+
+ Instance OrgNDR b n Γ Δ : @ND_Relation _ (OrgR b n Γ Δ) :=
+ { ndr_eqv := fun a b f g => (unOrgND _ _ _ _ _ _ f) === (unOrgND _ _ _ _ _ _ g) }.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+ (*
+ Hint Constructors Rule_Flat.
+
+ Definition SystemFC_SC n : @SequentCalculus _ (RuleSystemFCa n) _ (mkJudg Γ Δ).
+ apply Build_SequentCalculus.
+ intro a.
+ induction a.
+ destruct a.
+ apply nd_rule.
+ destruct l.
+ apply sfc_flat with (r:=RVar _ _ _ _).
+ auto.
+ apply nd_rule.
+ apply sfc_flat with (r:=REmptyGroup _ _).
+ auto.
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ eapply nd_comp; [ eapply nd_prod | idtac ].
+ apply IHa1.
+ apply IHa2.
+ apply nd_rule.
+ apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
+ auto.
+ Defined.
+
+ Existing Instance SystemFC_SC.
+
+ Lemma systemfc_cut n : ∀a b c,
+ ND (RuleSystemFCa n) ([Γ > Δ > a |- b],, [Γ > Δ > b |- c]) [Γ > Δ > a |- c].
+ intros.
+ admit.
+ Defined.
+
+ Lemma systemfc_cutrule n
+ : @CutRule _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfc n) (SystemFC_SC n).
+ apply Build_CutRule with (nd_cut:=systemfc_cut n).
+ admit.
+ admit.
+ admit.
+ Defined.
+
+ Definition systemfc_left n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > a,, b |- a,, c].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ eapply nd_comp; [ eapply nd_prod | idtac ].
+ Focus 3.
+ apply nd_rule.
+ apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
+ auto.
+ idtac.
+ apply nd_seq_reflexive.
+ apply nd_id.
+ Defined.
+
+ Definition systemfc_right n a b c : ND (RuleSystemFCa n) [Γ > Δ > b |- c] [Γ > Δ > b,,a |- c,,a].
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
+ eapply nd_comp; [ eapply nd_prod | idtac ].
+ apply nd_id.
+ apply (nd_seq_reflexive a).
+ apply nd_rule.
+ apply sfc_flat with (r:=RBindingGroup _ _ _ _ _ _ ).
+ auto.
+ Defined.
+*)
+(*
+ Definition systemfc_expansion n
+ : @SequentExpansion _ (RuleSystemFCa n) _ (mkJudg Γ Δ) (ndr_systemfca n) (SystemFC_SC n) (systemfc_cutrule n).
+ Check (@Build_SequentExpansion).
+apply (@Build_SequentExpansion _ _ _ _ (ndr_systemfca n) _ _ (systemfc_left n) (systemfc_right n)).
+ refine {| se_expand_left:=systemfc_left n
+ ; se_expand_right:=systemfc_right n |}.
+
+*)
+
+ (* 5.1.2 *)
+ Instance SystemFCa n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true n Γ Δ) :=
+ { pl_eqv := OrgNDR true n Γ Δ
+ ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
+ ; pl_sc := _
+ ; pl_subst := _
+ ; pl_sequent_join := _
+ }.
+ apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
+ apply nd_rule; apply org_fc; apply nd_rule; simpl. apply (RURule _ _ _ _ (RCossa _ a b c)).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RAssoc _ a b c)).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RCanL _ a )).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RCanR _ a )).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RuCanL _ a )).
+ apply nd_rule; apply org_fc; apply nd_rule; simpl; apply (RURule _ _ _ _ (RuCanR _ a )).
+ Admitted.
+
+ (* "flat" SystemFC: no brackets allowed *)
+ Instance SystemFC Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR true O Γ Δ) :=
+ { pl_eqv := OrgNDR true O Γ Δ
+ ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
+ ; pl_sc := _
+ ; pl_subst := _
+ ; pl_sequent_join := _
+ }.
+ Admitted.
+
+ (* 5.1.3 *)
+ Instance PCF n Γ Δ : @ProgrammingLanguage _ _ (@mkUJudg Γ Δ) (OrgR false n Γ Δ) :=
+ { pl_eqv := OrgNDR false n Γ Δ
+ ; pl_tsr := _ (*@TreeStructuralRules Judg Rule T sequent*)
+ ; pl_sc := _
+ ; pl_subst := _
+ ; pl_sequent_join := _
+ }.
+ apply Build_TreeStructuralRules; intros; unfold eqv; unfold hom; simpl.
+ apply nd_rule; apply org_pcf; simpl; exists (RCossa _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RAssoc _ a b c); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RCanL _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RCanR _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RuCanL _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ apply nd_rule; apply org_pcf; simpl; exists (RuCanR _ a ); apply (PCF_RURule [_>>_>_|-_] [_>>_>_|-_]).
+ Admitted.
+
+(*
+ Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
+ match t with
+(* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
+ | _ => code2garrow0 ec unitType t
+ end.
+ Opaque code2garrow.
+ Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
+ match ty as TY in RawHaskType _ K return RawHaskType TV K with
+ | TCode ec t => code2garrow _ ec t
+ | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
+ | TAll _ f => TAll _ (fun tv => typeMap (f tv))
+ | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
+ | TVar _ v => TVar v
+ | TArrow => TArrow
+ | TCon tc => TCon tc
+ | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
+ end.
+
+ Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
+ match lht with
+(* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*)
+ | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
+ end.
+*)
+
+ (* gathers a tree of guest-language types into a single host-language types via the tensor *)
+ Definition tensorizeType {Γ} (lt:Tree ??(LeveledHaskType Γ ★)) : HaskType Γ ★.
+ admit.
+ Defined.
+
+ Definition mkGA {Γ} : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★.
+ admit.
+ Defined.
+
+ Definition guestJudgmentAsGArrowType {Γ}{Δ} (lt:UJudg Γ Δ) : LeveledHaskType Γ ★ :=