Let x0 of type ι be given.
Apply unknownprop_56a3846d90f4ab1e1cdbc7eded30831439b09ed314019fdcbda6415f78b5a7c9 with
λ x1 x2 . ad280.. (add_SNo x2 (28f8d.. x0)) (add_SNo (d634d.. 0) (d634d.. x0)) = x0.
Apply unknownprop_83b1da2d18321ff78f0ba79977e134354a0cd5daef142de6498660d639616d8d with
λ x1 x2 . ad280.. (add_SNo 0 (28f8d.. x0)) (add_SNo x2 (d634d.. x0)) = x0.
Apply add_SNo_0L with
28f8d.. x0,
λ x1 x2 . ad280.. x2 (add_SNo 0 (d634d.. x0)) = x0 leaving 2 subgoals.
Apply unknownprop_62ffbce17a1080b510b3d10f88e78f4b8e9088a2c54409ce0c70e91f74a9fd08 with
x0.
The subproof is completed by applying H0.
Apply add_SNo_0L with
d634d.. x0,
λ x1 x2 . ad280.. (28f8d.. x0) x2 = x0 leaving 2 subgoals.
Apply unknownprop_f319423ed101339f42129d35c36f78ec84ab916352e52ec279686150bcbdfec5 with
x0.
The subproof is completed by applying H0.
Let x1 of type ι → ι → ο be given.
Apply unknownprop_5b83866c440783e0b1a158e0891e967d7f7864776be8302794e7cb2317ac7efc with
x0,
λ x2 x3 . x1 x3 x2.
The subproof is completed by applying H0.