+ Focus 2.
+ eapply nd_rule.
+ eapply RArrange.
+ apply RExch.
+
+ eapply nd_comp.
+ Focus 2.
+ eapply nd_rule.
+ apply q''.
+
+ idtac.
+ clear q'' q'.
+ eapply nd_comp.
+ apply nd_rlecnac.
+ apply nd_prod.
+ apply nd_id.
+ apply q.
+ Defined.
+
+(*
+ Notation "` x" := (take_lev _ x) (at level 20).
+ Notation "`` x" := (mapOptionTree unlev x) (at level 20).
+ Notation "``` x" := (drop_lev _ x) (at level 20).
+*)
+ Definition garrowfy_arrangement' :
+ forall Γ (Δ:CoercionEnv Γ)
+ (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
+ ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
+
+ intros Γ Δ ec lev.
+ refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
+ ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] :=
+ match r as R in Arrange A B return
+ ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]]
+ with
+ | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
+ | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
+ | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
+ | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
+ | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
+ | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
+ | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
+ | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
+ | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
+ | RLeft a b c r' => let case_RLeft := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
+ | RRight a b c r' => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
+ | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
+ end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
+
+ destruct case_RComp.
+ set (take_lev (ec :: lev) a) as a' in *.
+ set (take_lev (ec :: lev) b) as b' in *.
+ set (take_lev (ec :: lev) c) as c' in *.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply
+ (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply r2'.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply
+ (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ eapply nd_prod.
+ apply r1'.
+ apply ga_comp.
+ Defined.
+
+ Definition garrowfy_arrangement :
+ forall Γ (Δ:CoercionEnv Γ) n
+ (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
+ ND Rule
+ [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
+ |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
+ [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2)
+ |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]].
+ intros.
+ refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
+ apply nd_rule.
+ apply RArrange.
+ refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
+ match r as R in Arrange A B return
+ Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A))
+ (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with
+ | RCanL a => let case_RCanL := tt in RCanL _
+ | RCanR a => let case_RCanR := tt in RCanR _
+ | RuCanL a => let case_RuCanL := tt in RuCanL _
+ | RuCanR a => let case_RuCanR := tt in RuCanR _
+ | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
+ | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
+ | RExch a b => let case_RExch := tt in RExch _ _
+ | RWeak a => let case_RWeak := tt in RWeak _
+ | RCont a => let case_RCont := tt in RCont _
+ | RLeft a b c r' => let case_RLeft := tt in RLeft _ (garrowfy _ _ r')
+ | RRight a b c r' => let case_RRight := tt in RRight _ (garrowfy _ _ r')
+ | RComp a b c r1 r2 => let case_RComp := tt in RComp (garrowfy _ _ r1) (garrowfy _ _ r2)
+ end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
+ Defined.
+
+ Definition flatten_arrangement :
+ forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
+ ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
+ (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
+ intros.
+ simpl.
+ set (getjlev succ) as succ_lev.
+ assert (succ_lev=getjlev succ).
+ reflexivity.
+
+ destruct succ_lev.