proposition: Lemma commsqstrtocomplxstr {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (z : Z) (h : commsqstr f g (λ x : X, tt) (λ t : unit, z)) : complxstr f g z.
proof: Proof. intros. assumption. Defined.
imports: UniMath.Foundations.Preamble