The type of All_fold_app_inv is
∀ {A : Type} {P : list A → A → Type} (Γ Δ : list A),
All_fold P (Γ ++ Δ) ->
All_fold P Δ × All_fold (λ Γ0 : list A => P (Γ0 ++ Δ)) Γ
Args: {A}%type_scope {P}%function_scope (Γ Δ)%list_scope _
Constant MetaRocq.Utils.All_Forall.All_fold_app_inv
which is the one of All_X_app for All and Alli.
Conversely, for the _app which corresponds to the usual _app_inv
The type of
All_fold_app_inviswhich is the one of
All_X_appforAllandAlli.Conversely, for the
_appwhich corresponds to the usual_app_inv