proposition: Lemma O_concat {A : Type} {a0 a1 a2 : A} : O (a0 = a1) -> O (a1 = a2) -> O (a0 = a2).
proof: Proof. intros p q. strip_reflections. exact (to O _ (p @ q)). Defined.
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout