Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 . (λ x1 . True) x0 ⟶ ∀ x1 . x1 ⊆ x0 ⟶ (λ x2 . True) x1
Let x0 of type ι be given.
Assume H0: (λ x1 . True) x0.
Let x1 of type ι be given.
Assume H1: x1 ⊆ x0.
The subproof is completed by applying TrueI.
Claim L1: ∀ x0 . (λ x1 . True) x0 ⟶ ∀ x1 . (λ x2 . True) x1 ⟶ (λ x2 . True) (setprod x0 x1)
Let x0 of type ι be given.
Assume H1: (λ x1 . True) x0.
Let x1 of type ι be given.
Assume H2: (λ x2 . True) x1.
The subproof is completed by applying TrueI.
Apply unknownprop_a58587398f78cc19e584d164063d8a42566021285e8019a61cbb09a5b9caeb5a with λ x0 . True leaving 3 subgoals.
The subproof is completed by applying unknownprop_dcf5739aa5fe0adc626fd983737b233fe68652dff14c53b3d75823dcf2542d41.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
■