Apply unknownprop_70eb6d5c4e81105a9bb6d85a6ba8b693c19edf8ca2663bb07fea19af949fed82 with
λ x0 . True,
HomSet,
λ x0 . lam_id x0,
λ x0 x1 x2 x3 x4 . lam_comp x0 x3 x4 leaving 3 subgoals.
The subproof is completed by applying unknownprop_dcf5739aa5fe0adc626fd983737b233fe68652dff14c53b3d75823dcf2542d41.
The subproof is completed by applying unknownprop_e96f8cfa8459ba8da320317d59e27dfaa43e033527a319da7d720ca224964e29.
The subproof is completed by applying unknownprop_2c4f22a91db29194c445bcd6d03bd4d8a28e2ca068110adc6df3c2eb893080af.