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_910f270f5569d9b3d1b399a0d821e706f62672ed8ac07f2a600977372b2a7f17 with x0, x1, x2, ChurchNum_ii_2 ChurchNum2 x0 x3, λ x4 x5 . x5 = ChurchNum_ii_2 ChurchNum2 x0 (ChurchNum_ii_2 ChurchNum2 x0 (x2 x3)) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_1614b543c6d96eeda0a488900213094a8fd1c045e7cd1981f3f7be2de773b0b2 with x0, x1, x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_910f270f5569d9b3d1b399a0d821e706f62672ed8ac07f2a600977372b2a7f17 with x0, x1, x2, x3, λ x4 x5 . ChurchNum_ii_2 ChurchNum2 x0 x5 = ChurchNum_ii_2 ChurchNum2 x0 (ChurchNum_ii_2 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.