forall (f : LocalGenerators) (X : Type) (P : Localize f X -> Type) (loc' : forall x, P (loc x)) (islocal' : forall i, ooExtendableAlong_Over (f i) (fun _ => Localize f X) (fun _ => P) (islocal_localize f X i)) i n, apD_extendable_eq n (fun _ => Localize f X) (f i) (islocal_localize f X i n) (fun _ => P) (fun _ => Localize_ind f X P loc' islocal') (islocal' i n).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.