Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
In x0 x1,
Subq x1 x0,
ordinal (binintersect x0 x1) leaving 3 subgoals.
Apply unknownprop_682983ef060476485fcd03b6da6255e287c5314c9013030e2a8b79c1fa302a8c with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_5afda972c78302d86ad70171f9367780fa0c3403baf81f9e7aa674a8a6ec4541 with
x0,
x1,
λ x2 x3 . ordinal x3 leaving 2 subgoals.
Apply unknownprop_5af24edc592c6d7fa3cf53e40211635bbed8f39380469ac8aef3490ee700739c with
x1,
x0 leaving 2 subgoals.
Apply unknownprop_e682831a7124f89af4a1b1d248afbcd452dfbbb9d90b9a88db6885fe36808b65 with
x1.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
Apply unknownprop_de75d6825d81b7a38884e6d5bfefe1b968fb72336b8dd0437226d27d493a019a with
x0,
x1,
λ x2 x3 . ordinal x3.
Apply unknownprop_5afda972c78302d86ad70171f9367780fa0c3403baf81f9e7aa674a8a6ec4541 with
x1,
x0,
λ x2 x3 . ordinal x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.