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