Proofgold Proof

pf
Apply orIL with ChurchBoolTru = ChurchBoolTru, ChurchBoolTru = ChurchBoolFal. Let x0 of type (ι → ι → ι) → (ι → ι → ι) → ο be given. Assume H0: x0 ChurchBoolTru ChurchBoolTru. The subproof is completed by applying H0. ■