Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_f1b4b3f3609f7bbf0bc8735b08d44bfebb6a6346e99882a47fb54ee009e3ab08 with
λ x3 x4 . add_nat x0 x4 = ordsucc (ordsucc x0).
The subproof is completed by applying unknownprop_73c08fd5307f656249c9bc1b76ac9a0b21c5e7a3f5a4e3dad32d46dffb7bc549 with x0.
Apply L3 with
λ x3 x4 . equip (binrep x1 x2) x3.
Apply unknownprop_2cd90315ae9a4526fbcc7895b90453e88083a713b942f41e9949e0a524233d5f with
x0,
1,
x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
The subproof is completed by applying H1.
The subproof is completed by applying H2.