O_leq_lift_accrsu@{a i1 i2} (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{IsAccRSU@{a i1} O1} `{O_leq@{i1 i2 i2} O1 O2} : O_leq@{i2 i2 i2} (lift_accrsu@{a i1 i2} O1) O2. Proof. intros B B_inO1. apply (inO_leq@{i1 i2 i2} O1 O2). apply (snd (inO_iff_islocal O1 B)). intros i. specialize (B_inO1 i). apply (lift_ooextendablealong@{a a a a a a i2 i1 i2 i2 i1} (acc_lgen O1 i) (fun _ => B)). exact B_inO1. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.