+ destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+ rewrite <- e.
+ simpl.
+ apply AId.
+ unfold take_arg_types_as_tree.
+ Opaque take_arg_types_as_tree.
+ simpl.
+ destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
+ simpl.
+ replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
+ apply ACanR.
+ apply phoas_extensionality.
+ reflexivity.
+ apply (Prelude_error "should not be possible").
+ Defined.
+ Transparent take_arg_types_as_tree.
+
+ Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
+ Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
+ ([tx @@ lev],,take_arg_types_as_tree te @@@ lev).
+ intros.
+ destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+ rewrite <- e.
+ simpl.
+ apply AId.
+ unfold take_arg_types_as_tree.
+ Opaque take_arg_types_as_tree.
+ simpl.
+ destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
+ simpl.
+ replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
+ apply AuCanR.
+ apply phoas_extensionality.
+ reflexivity.
+ apply (Prelude_error "should not be possible").
+ Defined.
+ Transparent take_arg_types_as_tree.