Let x0 of type ι be given.
Apply unknownprop_485b5a544f4a752392d62c01e55a5e36a8748d64fd7af6f27349bd2453284446 with
x0,
λ x1 . u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x1 ∈ u16 leaving 17 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_5652f21220a21736c3c1c7ff394952ea63f98e4255215cdb9aaab91866efe7dd.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_2af8bf40bf7eaefd36fa12e21921eb2aeb029dbe2775546e49d5225f179719d9.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_fff531c49970071934428d0aef9046ef564b1c688918cc28a68137a9f7d29720.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_c38dc1b25a0e2dc5936848fac54d16b82c023e49a17d0d1875549efe638d7dec.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_64382522dade5b30fc9c1f845f10dec6adec6991c810bee97f2f66f396cf6712.
Apply unknownprop_b4b0b30bf8e5ff91ed4869311536b86e18ba1e4d9dcdabf73d46693ed9a5b67b with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_7f2d06b1efe37247a690b4e859e3aaf365f1da38cf576ae8a74607a7521a1608.
Apply unknownprop_8a85de05c64795068871a87d3b06ba1e5395c94812285b09588df3e01a1e0ea3 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_146ef1143e471cfbb8d96545c2df24929043ca109ec4a7c8c78dd73fb371c488.
Apply unknownprop_c0eb4e3448ef31f6408883194d369de2b67b2c3b8eb9ad88a4d52d9ee850a560 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_57616fbbcabc28eb1fb6407d841dda3edd107d79e8fcb804834746df27c3a6ca.
Apply unknownprop_f74f5074ad12d57b1f85300d32210524157b09a0919ee38128acf015331c35f0 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_4eba3f0917ffb7ab4575d03fa353c824d8d4f151df45c3ade8f1ca296d4cc0ee.
Apply unknownprop_4e46240fa21fb39b84708f415e3b21cc616773a08b926976627048ab8fc29078 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_f46bab0aaac49b12c19f821162ddb9736708dc036bc97f4e4318712d56c44f37.
Apply unknownprop_29ccb5c4e7950928d647b0941425c5e64d69ebaaed74cba3c055174a14ae4c5b with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_ae3e46fe1608a88c13cfd94c7c4f636604e089dbe99822d5f16bc7323d0026af.
Apply unknownprop_9b334a439f93d75505077dcc1fe4c60157a3105589338dee138085e931431815 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_96f337a74f7b868e3a36513c42dd4d06e5187cd640ec479c0814272a65371d35.
Apply unknownprop_c21ba5695b1d95da76a10179e8a88254ffe230dfdf6a6df2f9b5ee9d0562acd5 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_279fe6eb4b3ee21a0be2650377dfae573b176ecc12970f64812a6be52f3acfb9.
Apply unknownprop_ffb148d18f258a6f2e8b9af29fd6bea695bdd737e09f02c9ed6ace715b49951e with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_b79a9b70d083f86c18981643e47c737565f20b5a8d9333bff56376600ec4e5a4.
Apply unknownprop_5236a0eac529d064f7d4286c27876c5cf1e6aa8482e677668f1eb521e10e6be9 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_f388ecefb2fe6e2e313ca750501544c7c4c2bb13327baa7d874fe8dbdb4dc6e4.
Apply unknownprop_991646d91cf5e2f3eac2db7f6827c54bc2cbba5f33c26bd9a4d54268790991f8 with
λ x1 x2 . x2 ∈ u16.
The subproof is completed by applying unknownprop_6e0619c3165595ae4977f8d2ecfade1c59a6348e91d9234d9239b2fe0fb04ddf.