Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ο be given.
Apply unknownprop_f95c994468e053a5f3a3fd1414f88d890e2044d71aa0b2aca169453322d6ef34 with
236dc.. x0 x1,
x1 = f6a32.. (236dc.. x0 x1),
λ x3 x4 . x2 x4 x3 leaving 2 subgoals.
Apply unknownprop_a11dfa210cd480918339ec3ee480411b7f4945c0aeef474c01ca879d15816c74 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_af5a8211ff947ff893b5035a5559a8e74e1503a79511eecb1f7a8d29e2eae278 with
x0,
x1,
λ x3 x4 . 236dc.. x0 x1 = 236dc.. x4 (f6a32.. (236dc.. x0 x1)) ⟶ x1 = f6a32.. (236dc.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_1a9222940441343d3950b4eb89809bcf78424e1f44385bb97272c35b14b298d2 with
x0,
x1,
x0,
f6a32.. (236dc.. x0 x1) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.