Theorem hfsqstrtofibseqstr {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (hf : hfsqstr (λ t : unit, z) g (λ x : X, tt) f) : fibseqstr f g z. Proof. intros. split with (pr1 hf). set (ff := ezmap f g z (pr1 hf)). set (ggff := weqZtohfp (λ t : unit, z) g (λ x : X, tt) f hf). set (gg := weqhfibertohfp g z). apply (twooutof3a ff gg (pr2 ggff) (pr2 gg)). Defined.