+ apply X.
+ apply first_nd.
+ Defined.
+
+ Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
+ ND Rule
+ [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
+ [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
+ apply nd_prod.
+ apply nd_id.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
+ apply ga_second.
+ Defined.
+
+ Definition secondify : ∀ Γ Δ ec lev a b c Σ,
+ ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
+ ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
+ intros.
+ eapply nd_comp.
+ apply X.
+ apply second_nd.
+ Defined.
+
+ Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x,
+ ND Rule
+ [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ]
+ [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply ga_first.
+
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply postcompose.
+ apply ga_uncancell.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+ apply precompose.
+ Defined.
+
+ (* useful for cutting down on the pretty-printed noise
+
+ 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 flatten_arrangement' :
+ forall Γ (Δ:CoercionEnv Γ)
+ (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
+ ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
+ (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
+
+ intros Γ Δ ec lev.
+ refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
+ ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
+ (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
+ (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
+ match r as R in Arrange A B return
+ ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
+ (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
+ (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
+ with
+ | AId a => let case_AId := tt in ga_id _ _ _ _ _
+ | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _
+ | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _
+ | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _
+ | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
+ | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
+ | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
+ | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _
+ | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _
+ | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _
+ | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
+ | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
+ | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
+ end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
+
+ destruct case_AComp.
+ set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
+ set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
+ set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply
+ (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply r2'.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ eapply nd_prod.
+ apply r1'.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+ apply ga_comp.
+ Defined.
+
+ Definition flatten_arrangement :
+ forall Γ (Δ:CoercionEnv Γ) n
+ (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
+ ND Rule
+ [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
+ |- [@ga_mk _ (v2t ec)
+ (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
+ (mapOptionTree (flatten_type ) succ) ]@nil]
+ [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
+ |- [@ga_mk _ (v2t ec)
+ (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
+ (mapOptionTree (flatten_type ) succ) ]@nil].
+ intros.
+ refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
+ apply nd_rule.
+ apply RArrange.
+ refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
+ match r as R in Arrange A B return
+ Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
+ (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
+ | AId a => let case_AId := tt in AId _
+ | ACanL a => let case_ACanL := tt in ACanL _
+ | ACanR a => let case_ACanR := tt in ACanR _
+ | AuCanL a => let case_AuCanL := tt in AuCanL _
+ | AuCanR a => let case_AuCanR := tt in AuCanR _
+ | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _
+ | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _
+ | AExch a b => let case_AExch := tt in AExch _ _
+ | AWeak a => let case_AWeak := tt in AWeak _
+ | ACont a => let case_ACont := tt in ACont _
+ | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r')
+ | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r')
+ | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2)
+ end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
+ Defined.
+
+ Definition flatten_arrangement'' :
+ forall Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
+ ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
+ (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
+ intros.
+ simpl.
+ destruct l.