Proofgold Proof

pf
Claim L0: ∀ x0 . True ⟶ ∀ x1 . True ⟶ True Let x0 of type ι be given. Assume H0: True. Let x1 of type ι be given. Assume H1: True. The subproof is completed by applying TrueI. Apply unknownprop_7e80016cd90eba8cfb22e412d51217cbc5f2eeece9405f5140e2181ec01c4b9a with λ x0 . True. The subproof is completed by applying L0. ■