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