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).
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).
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).
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).
set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
- eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ].
+ eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
apply nd_prod; [ idtac | eapply nd_id ].
eapply nd_rule; apply SFlat; eapply RArrange.
eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
apply nd_prod; [ idtac | eapply nd_id ].
eapply nd_rule; apply SFlat; eapply RArrange.