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