Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
4ae4a.. x1.
The subproof is completed by applying L5.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x0,
4ae4a.. x1,
λ x2 x3 . x3 = 4ae4a.. (bc82c.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L6.
Apply unknownprop_4a758bfc21a1092ca84ad655b19c880511c90a7d55bbab7352511dd41ae6678d with
x1,
x0,
λ x2 x3 . x3 = 4ae4a.. (bc82c.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x1,
x0,
λ x2 x3 . 4ae4a.. x3 = 4ae4a.. (bc82c.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H7.