Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι be given.
Apply prop_ext_2 with
decode_p (1216a.. x0 x1) x2,
x1 x2 leaving 2 subgoals.
Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with
x0,
x1,
x2.
The subproof is completed by applying H1.
Assume H1: x1 x2.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.