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_2d427e86e80080bca0cd1cdb7569c48ac3ebc7f720e53d0aef56ae9082c9d013 with λ x0 . True. The subproof is completed by applying L0. ■