Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply prop_ext_2 with
2b2e3.. (d2155.. x0 x1) x2 x3,
x1 x2 x3 leaving 2 subgoals.
Apply unknownprop_90f3556d2d4ac58e465c1776e50b6b2895f1687af1cce4cbfdbd2560fc5880d2 with
x0,
λ x4 . x0,
x1,
x2,
x3.
The subproof is completed by applying H2.
Assume H2: x1 x2 x3.
Apply unknownprop_f0ee0e0da1b09f2dfb62d73da9f7b08ad931aaf047c3bc215bf1dd6e512c41c1 with
x0,
λ x4 . x0,
x1,
x2,
x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.