Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_eb2dfcc61b297e9bd5334705d22ba206e3441f9f0cfc821c0488b814ec57c600 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_34004d936e9c770d7776a68f4fd89de16dd752c63a364055547f1f2fd867c6b6 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_9cdeca2a60d0177233427129e29ed2aec16e770191654a999da75532b00612a1 with
x1,
λ x2 x3 . x3 = x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply L4 with
λ x2 x3 . 1beb9.. x2 (f4dc0.. x1).
Apply unknownprop_90012ae02c7e97888ea4d0a930b01b500b9d0d1d1a0841df69b82a77726b906b with
f4dc0.. x1.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
x1.
The subproof is completed by applying L2.