Apply unknownprop_70eb6d5c4e81105a9bb6d85a6ba8b693c19edf8ca2663bb07fea19af949fed82 with
λ x0 . x0 ∈ prim6 (prim6 0),
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_ea08c803821fdb965d694deab91a57c59674f0d5893e9652ca739817958ed900.
The subproof is completed by applying unknownprop_6f1bce2f0b91cc4a4b01a9a909982b70ca9997251007f0b1f3a245e92f902fcd.
The subproof is completed by applying unknownprop_15e47c4df03b56c280c2c40875ac93a29c682865c9aaf758b6236b5102f1d6ad.