+ 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 RExch ].
+ 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 RExch ].
+ 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
+ | RId a => let case_RId := tt in ga_id _ _ _ _ _
+ | 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 flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
+ | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
+ | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
+ end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
+
+ destruct case_RComp.
+ 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 RCanL ].
+ 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 RuCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+ 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 RExch ].
+ 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
+ | RId a => let case_RId := tt in RId _
+ | 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 _ (flatten _ _ r')
+ | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
+ | RComp a b c r1 r2 => let case_RComp := tt in RComp (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.