proposition: Theorem twooutofsixw {X Y Z K : UU} {u : X -> Y} {v : Y -> Z} {w : Z -> K} (isuv : isweq (funcomp u v))(isvw : isweq (funcomp v w)) : isweq w.
proof: Proof. intros. exact (twooutof3b _ _ (twooutofsixv isuv isvw) isvw). Defined.
imports: UniMath.Foundations.Preamble