- apply (nd_llecnac ;; nd_prod IHX1 IHX2).
- clear IHX1 IHX2 X1 X2.
- apply (@snd_cut _ _ _ _ (pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))).
-
- (* nd_cancell becomes RVar;;RuCanL *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_cancelr becomes RVar;;RuCanR *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_llecnac becomes RVar;;RCanL *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_rlecnac becomes RVar;;RCanR *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_assoc becomes RVar;;RAssoc *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- (* nd_cossa becomes RVar;;RCossa *)
- eapply nd_comp;
- [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
- apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
- apply Flat_RArrange.
-
- destruct r as [r rp].
- rename h into h'.
- rename c into c'.
- rename r into r'.
-
- refine (match rp as R in @Rule_PCF _ _ _ H C _
- return
- ND (OrgR Γ Δ) []
- [sequent (mapOptionTree guestJudgmentAsGArrowType H @@@ nil)
- (mapOptionTree guestJudgmentAsGArrowType C @@@ nil)]
- with
- | PCF_RArrange h c r q => let case_RURule := tt in _
- | PCF_RLit lit => let case_RLit := tt in _
- | PCF_RNote Σ τ n => let case_RNote := tt in _
- | PCF_RVar σ => let case_RVar := tt in _
- | PCF_RLam Σ tx te => let case_RLam := tt in _
- | PCF_RApp Σ tx te p => let case_RApp := tt in _
- | PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _
- | PCF_RJoin b c d e => let case_RJoin := tt in _
- | PCF_RVoid => let case_RVoid := tt in _
- (*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*)
- (*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*)
- end); simpl in *.
- clear rp h' c' r'.
-
- rewrite (unlev_lemma h (ec::nil)).
- rewrite (unlev_lemma c (ec::nil)).
- destruct case_RURule.
- refine (match q as Q in Arrange H C
- return
- H=(h @@@ (ec :: nil)) ->
- C=(c @@@ (ec :: nil)) ->
- ND (OrgR Γ Δ) []
- [sequent
- [ga_type (ga_rep (mapOptionTree unlev H)) (ga_rep r) @@ nil ]
- [ga_type (ga_rep (mapOptionTree unlev C)) (ga_rep r) @@ nil ] ]
- with
- | RLeft a b c r => let case_RLeft := tt in _
- | RRight a b c r => let case_RRight := tt in _
- | RCanL b => let case_RCanL := tt in _
- | RCanR b => let case_RCanR := tt in _
- | RuCanL b => let case_RuCanL := tt in _
- | RuCanR b => let case_RuCanR := tt in _
- | RAssoc b c d => let case_RAssoc := tt in _
- | RCossa b c d => let case_RCossa := tt in _
- | RExch b c => let case_RExch := tt in _
- | RWeak b => let case_RWeak := tt in _
- | RCont b => let case_RCont := tt in _
- | RComp a b c f g => let case_RComp := tt in _
- end (refl_equal _) (refl_equal _));
- intros; simpl in *;
- subst;
- try rewrite <- unlev_lemma in *.
-
- destruct case_RCanL.
- apply magic.
- apply ga_uncancell.
-
- destruct case_RCanR.
- apply magic.
- apply ga_uncancelr.
+ Focus 2.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ eapply nd_llecnac | idtac ].
+ eapply nd_prod.
+ apply pfb.
+ clear pfb.
+ apply postcompose'.
+ eapply nd_comp.
+ apply pfa.
+ clear pfa.
+ apply boost.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+ apply precompose'.
+ apply ga_uncancelr.
+ apply nd_id.
+ Defined.
+
+ Definition arrange_brak : forall Γ Δ ec succ t,
+ ND Rule
+ [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
+ [(@ga_mk _ (v2t ec) []
+ (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ)))
+ @@ nil] |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
+ [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
+ intros.
+ unfold drop_lev.
+ set (@arrange' _ succ (levelMatch (ec::nil))) as q.
+ set (arrangeMap _ _ flatten_leveled_type q) as y.
+ eapply nd_comp.
+ Focus 2.
+ eapply nd_rule.
+ eapply RArrange.
+ apply y.
+ idtac.
+ clear y q.
+ simpl.
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ apply nd_prod.
+ Focus 2.
+ apply nd_id.
+ idtac.
+ induction succ; try destruct a; simpl.
+ unfold take_lev.
+ unfold mkTakeFlags.
+ unfold mkFlags.
+ unfold bnot.
+ simpl.
+ destruct l as [t' lev'].
+ destruct lev' as [|ec' lev'].
+ simpl.
+ apply ga_id.
+ unfold levelMatch.
+ set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
+ destruct q.
+ inversion e; subst.
+ simpl.
+ apply nd_rule.
+ unfold flatten_leveled_type.
+ simpl.
+ unfold flatten_type.
+ apply RVar.
+ simpl.
+ apply ga_id.
+ apply ga_id.
+ unfold take_lev.
+ simpl.
+ apply ga_join.
+ apply IHsucc1.
+ apply IHsucc2.
+ Defined.