Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ιι be given.
Let x1 of type ιο be given.
Let x2 of type ιι be given.
Assume H0: ∀ x3 . x1 x3x1 (x0 x3).
Assume H1: ∀ x3 . x1 x3x2 (x0 x3) = x0 (x2 x3).
Let x3 of type ι be given.
Assume H2: x1 x3.
Apply unknownprop_25e71d8a7ad20837122ea1d4ff51220449571353b61bd172f7ce85161686ccac with x0, x1, x2, ChurchNum_ii_4 ChurchNum2 x0 x3, λ x4 x5 . x5 = ChurchNum_ii_4 ChurchNum2 x0 (ChurchNum_ii_4 ChurchNum2 x0 (x2 x3)) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_e93a8c6aa6f443714903366c406c66ee5568ab35bb2d12e6033aa07bd1f73b7d with x0, x1, x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_25e71d8a7ad20837122ea1d4ff51220449571353b61bd172f7ce85161686ccac with x0, x1, x2, x3, λ x4 x5 . ChurchNum_ii_4 ChurchNum2 x0 x5 = ChurchNum_ii_4 ChurchNum2 x0 (ChurchNum_ii_4 ChurchNum2 x0 (x2 x3)) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x4 of type ιιο be given.
The subproof is completed by applying H3.