Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_62141d6d964f50dd758bf190f29372c5be04f6855040150df577bd62bb4a5ef6 with
1ce4f.. x0,
1ce4f.. x1,
λ x2 : ι → ο . x2 = 1ce4f.. x0 ⟶ In x0 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_44e793277f45678da94c2013fcdf0d451e96978737d7b9c11a549b9b802461d1 with
x2,
x0,
λ x3 x4 . In x3 x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Let x2 of type (ι → ο) → (ι → ο) → ο be given.
The subproof is completed by applying H1.