Let x0 of type ι be given.
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with
x0.
The subproof is completed by applying H0.
Apply PNoEq_tra_ with
e4431.. x0,
λ x1 . prim1 x1 (09072.. (4ae4a.. (e4431.. x0)) (λ x2 . and (prim1 x2 x0) (x2 = e4431.. x0 ⟶ ∀ x3 : ο . x3))),
λ x1 . and (prim1 x1 x0) (x1 = e4431.. x0 ⟶ ∀ x2 : ο . x2),
λ x1 . prim1 x1 x0 leaving 2 subgoals.
Apply PNoEq_antimon_ with
λ x1 . prim1 x1 (09072.. (4ae4a.. (e4431.. x0)) (λ x2 . and (prim1 x2 x0) (x2 = e4431.. x0 ⟶ ∀ x3 : ο . x3))),
λ x1 . and (prim1 x1 x0) (x1 = e4431.. x0 ⟶ ∀ x2 : ο . x2),
4ae4a.. (e4431.. x0),
e4431.. x0 leaving 3 subgoals.
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with
e4431.. x0.
The subproof is completed by applying L1.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with
e4431.. x0.
Apply unknownprop_8ab8782df8e80eb287fd4c918f7b35b584f8954d0de002e6915e8d87848fc5f4 with
4ae4a.. (e4431.. x0),
λ x1 . and (prim1 x1 x0) (x1 = e4431.. x0 ⟶ ∀ x2 : ο . x2).
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with
e4431.. x0.
The subproof is completed by applying L1.
Apply PNoEq_sym_ with
e4431.. x0,
λ x1 . prim1 x1 x0,
λ x1 . and (prim1 x1 x0) (x1 = e4431.. x0 ⟶ ∀ x2 : ο . x2).
The subproof is completed by applying PNo_extend0_eq with
e4431.. x0,
λ x1 . prim1 x1 x0.