Open
Description
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
Metadata
Metadata
Assignees
Labels
No labels