proposition: Lemma subtype_inc_comp {X:UU} {S T U : hsubtype X} (i:S⊆T) (j:T⊆U) (s:S) : subtype_inc j (subtype_inc i s) = subtype_inc (λ x, j x ∘ i x) s.
proof: Proof. reflexivity. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions