Skip to content

Instantly share code, notes, and snippets.

@pedrominicz

pedrominicz/Lean.hs

Last active Oct 13, 2020
Embed
What would you like to do?
A lean prover for minimal logic.
module Lean where
-- http://ceur-ws.org/Vol-2271/paper1.pdf
import Control.Monad
import Data.Bifunctor
data Term
= Var Char
| Impl Term Term
deriving (Eq, Show)
prove :: Term -> Bool
prove = not . null . ljt []
ljt :: [Term] -> Term -> [Term]
ljt env t
| elem t env = return t
ljt env (Impl a b) = ljt (a : env) b
ljt env t = do
(Impl a b, env) <- select env
case a of
Var a -> do
guard $ elem (Var a) env
ljt (b : env) t
Impl c d -> do
ljt (Impl d b : env) (Impl c d)
ljt (b : env) t
select :: [a] -> [(a, [a])]
select (x:xs) = (x, xs) : map (second (x:)) (select xs)
select [] = []
(~>) :: Term -> Term -> Term
(~>) = Impl
infixr 6 ~>
a, b, c :: Term
a = Var 'a'
b = Var 'b'
c = Var 'c'
-- prove $ a ~> a
-- prove $ a ~> b ~> a
-- prove $ (a ~> b ~> c) ~> (a ~> b) ~> a ~> c
-- prove $ (a ~> b) ~> (c ~> a) ~> c ~> b
-- prove $ (a ~> b ~> c) ~> b ~> a ~> c
-- prove $ (a ~> a ~> b) ~> a ~> b
-- prove $ ((a ~> b ~> a) ~> c) ~> c
-- prove $ ((a ~> b) ~> b ~> c) ~> b ~> c
This file has been truncated, but you can view the full file.
module TestCompleteness where
import Lean
d, e, f :: Term
d = Var 'd'
e = Var 'e'
f = Var 'f'
tests :: [Bool]
tests =
[ prove $ a ~> a
, prove $ a ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> a ~> a
, prove $ a ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> a ~> a ~> a
, prove $ a ~> ((a ~> a) ~> a) ~> a
, prove $ a ~> (a ~> a ~> a) ~> a
, prove $ a ~> (a ~> a) ~> a ~> a
, prove $ a ~> a ~> (a ~> a) ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ (a ~> (a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a ~> a ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> a ~> (a ~> a) ~> a
, prove $ a ~> (((a ~> a) ~> a) ~> a) ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ a ~> (a ~> (a ~> a) ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> a) ~> a
, prove $ a ~> (a ~> a ~> a) ~> a ~> a
, prove $ a ~> (a ~> a) ~> (a ~> a) ~> a
, prove $ a ~> a ~> (a ~> a ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> a ~> a
, prove $ (a ~> (a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (a ~> a ~> a ~> a) ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (a ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a) ~> a ~> a ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> a ~> (a ~> a ~> a) ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a ~> a) ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ a ~> (a ~> (a ~> a) ~> a ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> a) ~> a ~> a
, prove $ a ~> (a ~> a ~> a) ~> (a ~> a) ~> a
, prove $ a ~> (a ~> a ~> a) ~> a ~> a ~> a
, prove $ a ~> (a ~> a) ~> (a ~> a ~> a) ~> a
, prove $ a ~> a ~> (a ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a) ~> a
, prove $ ((((a ~> a) ~> a) ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a) ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ ((a ~> a ~> a) ~> a ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a ~> a) ~> a) ~> (a ~> a ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a ~> a) ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> (a ~> a) ~> a
, prove $ (a ~> (a ~> a) ~> a) ~> (a ~> a) ~> a ~> a
, prove $ (a ~> (a ~> a) ~> a) ~> a ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a ~> a) ~> a) ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> (a ~> a) ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> (a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> ((((a ~> a) ~> a) ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a) ~> (a ~> a ~> a) ~> a ~> a ~> a
, prove $ (a ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ (a ~> a) ~> a ~> (a ~> (a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> a ~> (a ~> a ~> a) ~> a ~> a
, prove $ a ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ a ~> ((a ~> a ~> a) ~> a ~> a ~> a) ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a
, prove $ a ~> (a ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> a) ~> a ~> a ~> a
, prove $ a ~> (a ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ a ~> (a ~> a) ~> (a ~> (a ~> a) ~> a) ~> a
, prove $ a ~> (a ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ a ~> a ~> (a ~> a ~> a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ ((a ~> a ~> a) ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a ~> a) ~> a) ~> a ~> (a ~> a ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a ~> a) ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> (a ~> a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> a ~> (a ~> a ~> a) ~> a ~> a
, prove $ (a ~> a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a
, prove $ (a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (a ~> a ~> a) ~> a ~> ((a ~> a ~> a) ~> a) ~> a
, prove $ (a ~> a ~> a) ~> a ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a ~> a) ~> a
, prove $ (a ~> a) ~> (a ~> a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ a ~> ((a ~> a ~> a) ~> a) ~> (a ~> a ~> a) ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ a ~> ((a ~> a) ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ a ~> (a ~> a ~> a ~> a ~> a) ~> a ~> a ~> a
, prove $ a ~> (a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a
, prove $ a ~> (a ~> a ~> a) ~> ((a ~> a ~> a) ~> a) ~> a
, prove $ a ~> (a ~> a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> a) ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a ~> (a ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ ((a ~> (a ~> a) ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a ~> a) ~> (a ~> a) ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a ~> a) ~> a ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> (a ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a ~> a ~> a) ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ (a ~> ((a ~> a) ~> a) ~> a) ~> a ~> ((a ~> a) ~> a) ~> a
, prove $ (a ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a ~> a
, prove $ (a ~> (a ~> a) ~> a ~> a) ~> a ~> (a ~> a) ~> a ~> a
, prove $ (a ~> (a ~> a) ~> a) ~> (a ~> a) ~> a ~> (a ~> a) ~> a
, prove $ (a ~> (a ~> a) ~> a) ~> a ~> (a ~> a) ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a ~> a
, prove $ (a ~> a ~> a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> a ~> a) ~> a ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> a ~> a) ~> a ~> a ~> a
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> a) ~> a ~> (a ~> a) ~> a
, prove $ (a ~> a) ~> (a ~> a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> a ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> a ~> (a ~> (a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> a ~> (a ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ a ~> (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> a
, prove $ a ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ a ~> (a ~> ((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ a ~> (a ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ a ~> (a ~> (a ~> a) ~> a) ~> (a ~> a) ~> (a ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a
, prove $ a ~> (a ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> a ~> a ~> a) ~> a ~> a
, prove $ a ~> (a ~> a) ~> (a ~> (a ~> a) ~> a ~> a) ~> a ~> a
, prove $ a ~> (a ~> a) ~> (a ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a ~> a) ~> (a ~> a) ~> a ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a ~> a) ~> a ~> (a ~> a) ~> a ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> a ~> a) ~> a ~> a ~> a ~> a
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> a ~> a ~> a) ~> a ~> a ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a ~> a) ~> (a ~> a) ~> a ~> a ~> a
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> a ~> a ~> a) ~> a ~> a ~> a
, prove $ ((((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ ((((a ~> a) ~> a) ~> a) ~> (a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a) ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> a) ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> a ~> (a ~> a) ~> a) ~> a ~> a ~> (a ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> a) ~> ((((a ~> a) ~> a) ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ ((a ~> (a ~> a) ~> a) ~> a ~> (a ~> a) ~> a) ~> a ~> (a ~> a) ~> a
, prove $ ((a ~> a ~> a) ~> a ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a ~> a
, prove $ ((a ~> a ~> a) ~> a ~> a ~> a) ~> a ~> (a ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a ~> a) ~> a) ~> (a ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> (((a ~> a) ~> a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ (a ~> a ~> a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a ~> a) ~> a ~> a ~> a) ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a ~> a) ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> (a ~> a ~> a) ~> ((a ~> a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> ((a ~> a ~> a) ~> a ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> (((a ~> a) ~> a ~> a) ~> a) ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ (a ~> a) ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> (a ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ a ~> (((a ~> a) ~> a) ~> a ~> (a ~> a) ~> a) ~> a ~> (a ~> a) ~> a
, prove $ a ~> ((a ~> a ~> a) ~> a ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ a ~> (a ~> a ~> a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a ~> a
, prove $ a ~> (a ~> a ~> a) ~> ((a ~> a ~> a) ~> a ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a) ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> (a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> ((a ~> a) ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> ((a ~> a) ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a) ~> ((((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a) ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ (((a ~> a ~> a) ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a) ~> a ~> (a ~> a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> ((((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ a ~> (((a ~> a ~> a) ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ (((a ~> a ~> a) ~> a ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a ~> a) ~> (a ~> a ~> a) ~> a ~> a ~> a
, prove $ (((a ~> a) ~> ((a ~> a) ~> a) ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> a
, prove $ ((a ~> (a ~> a ~> a) ~> a ~> a) ~> a ~> (a ~> a ~> a) ~> a ~> a) ~> a ~> (a ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> b ~> a ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> a) ~> b ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b) ~> ((a ~> a) ~> a ~> a) ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> ((a ~> a) ~> a ~> a) ~> b
, prove $ ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> ((a ~> a) ~> a ~> a) ~> b
, prove $ (((((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> ((a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b) ~> c ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> c ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> a) ~> ((a ~> a) ~> a ~> a) ~> b ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> b ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> a) ~> b ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a) ~> b ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> (((a ~> a) ~> a) ~> a ~> b) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> (a ~> ((a ~> a) ~> a) ~> b) ~> b
, prove $ (a ~> a ~> a) ~> ((a ~> a ~> a) ~> (a ~> a ~> a) ~> b) ~> b
, prove $ (a ~> a ~> a) ~> a ~> ((a ~> a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ (a ~> a ~> a) ~> a ~> ((a ~> a) ~> (a ~> a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> ((a ~> a) ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a ~> a) ~> ((a ~> a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a ~> a) ~> ((a ~> a) ~> (a ~> a ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> b ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> a ~> a) ~> ((a ~> a) ~> a) ~> b ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> b ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> b) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a ~> a) ~> b ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a ~> a) ~> b ~> a ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> b ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> (a ~> a) ~> a) ~> a ~> (a ~> a) ~> a) ~> b ~> a ~> (a ~> a) ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> b ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> (b ~> a ~> a) ~> c) ~> c
, prove $ (a ~> a ~> a) ~> ((a ~> a ~> a) ~> (a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> (a ~> a ~> a) ~> b) ~> a ~> b
, prove $ ((((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> a) ~> b) ~> b
, prove $ ((((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ (((a ~> a ~> a ~> a) ~> a ~> a ~> a ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> (a ~> a ~> a ~> a) ~> a ~> a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> (a ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> (((a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a ~> b) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> (a ~> (a ~> a) ~> b) ~> b
, prove $ (a ~> a ~> a ~> a) ~> ((a ~> a ~> a ~> a) ~> b) ~> b
, prove $ (a ~> a ~> a ~> a) ~> a ~> ((a ~> a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((((a ~> a) ~> (a ~> a) ~> a) ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((((a ~> a) ~> a) ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (((a ~> a) ~> a) ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> ((a ~> a) ~> a ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> (a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> (a ~> a) ~> a ~> b) ~> b
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> a ~> (a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> a ~> (a ~> (a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ a ~> (((a ~> a ~> a ~> a) ~> a ~> a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a ~> a ~> a) ~> ((a ~> a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a ~> b) ~> b
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> a ~> (a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a) ~> (a ~> (a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> b ~> c ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> a) ~> ((a ~> a) ~> a) ~> b ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> b ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> b ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> (a ~> a) ~> b ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a) ~> b ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> b ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> a ~> b ~> a
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> a ~> a) ~> b ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b ~> a
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b ~> a
, prove $ ((a ~> a ~> a) ~> a) ~> (a ~> a ~> a) ~> b ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a ~> a) ~> a) ~> b ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> a ~> b ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> a) ~> b ~> (a ~> a) ~> a
, prove $ a ~> (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> b ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> ((a ~> a) ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ (((a ~> a ~> a ~> a) ~> a ~> a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a ~> a ~> a) ~> ((a ~> a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a ~> b) ~> a ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> (a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> (a ~> a) ~> b) ~> a ~> b
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> a ~> b) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> ((a ~> a) ~> a) ~> b) ~> b
, prove $ (a ~> a ~> a) ~> a ~> ((a ~> a) ~> a ~> b) ~> b
, prove $ (a ~> a ~> a) ~> a ~> (a ~> (a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> a ~> a ~> b) ~> b
, prove $ (a ~> a) ~> a ~> (a ~> (a ~> a) ~> a ~> b) ~> b
, prove $ (a ~> a) ~> a ~> (a ~> a ~> (a ~> a) ~> b) ~> b
, prove $ a ~> (((a ~> a ~> a) ~> a ~> a) ~> a ~> b) ~> b
, prove $ a ~> (a ~> ((a ~> a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a ~> a ~> a ~> a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> a) ~> ((a ~> a) ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> a) ~> (a ~> (a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a) ~> (a ~> (a ~> a) ~> a ~> b) ~> b
, prove $ a ~> (a ~> a) ~> (a ~> a ~> (a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> a) ~> b ~> c ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> b ~> c ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a ~> a) ~> b ~> a ~> a
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> a) ~> b ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> b ~> a ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a ~> a) ~> b ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> b) ~> (a ~> a) ~> a ~> a
, prove $ (a ~> a ~> a ~> a ~> a) ~> a ~> b ~> a ~> a ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> (b ~> a ~> a) ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> a ~> a) ~> b ~> a ~> a ~> a ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> b) ~> (((a ~> a) ~> a ~> a) ~> a ~> a) ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b) ~> ((a ~> a) ~> a ~> a) ~> b
, prove $ ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> ((a ~> a) ~> a ~> a) ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b) ~> ((a ~> a) ~> a ~> a) ~> c ~> b
, prove $ ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> ((a ~> a) ~> a ~> a) ~> c ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> (b ~> (a ~> a) ~> a ~> a) ~> c) ~> c
, prove $ (((a ~> a) ~> a) ~> ((a ~> a) ~> a) ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ ((a ~> a ~> a) ~> (a ~> a ~> a) ~> b) ~> (a ~> a ~> a) ~> b
, prove $ (a ~> a) ~> (((a ~> a) ~> a) ~> a ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> ((a ~> a) ~> a) ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ a ~> ((a ~> a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a ~> a) ~> b
, prove $ a ~> ((a ~> a) ~> (a ~> a ~> a) ~> b) ~> (a ~> a ~> a) ~> b
, prove $ ((((a ~> a) ~> (a ~> a) ~> a) ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ ((((a ~> a) ~> a) ~> a) ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> (((a ~> a) ~> a) ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> (a ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> a) ~> ((a ~> a) ~> a ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ a ~> ((a ~> a) ~> (a ~> a) ~> a ~> b) ~> (a ~> a) ~> b
, prove $ a ~> ((a ~> a) ~> a ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ a ~> (a ~> (a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ (((a ~> a ~> a) ~> a ~> a) ~> a ~> b) ~> a ~> b
, prove $ (a ~> ((a ~> a ~> a) ~> a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a ~> a ~> a ~> a ~> a ~> b) ~> a ~> b
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> a ~> b) ~> a ~> b
, prove $ (a ~> a ~> a) ~> (a ~> (a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> a ~> b) ~> a ~> b
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> a ~> b) ~> a ~> b
, prove $ (a ~> a) ~> (a ~> a ~> (a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> b ~> a) ~> b ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ ((((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> b) ~> b
, prove $ (((a ~> a ~> a) ~> a ~> a ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> ((a ~> a) ~> a) ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ ((a ~> ((a ~> a) ~> a ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> (a ~> a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> (a ~> b) ~> b
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> (a ~> b) ~> b
, prove $ (a ~> a ~> a) ~> ((a ~> a ~> a) ~> b) ~> b
, prove $ (a ~> a ~> a) ~> a ~> ((a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((((a ~> a) ~> a) ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> b) ~> b
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> a ~> b) ~> b
, prove $ (a ~> a) ~> a ~> (a ~> (a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> a ~> (a ~> a ~> a ~> b) ~> b
, prove $ a ~> ((((a ~> a) ~> a ~> a) ~> a) ~> b) ~> b
, prove $ a ~> (((a ~> a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ a ~> (((a ~> a) ~> a) ~> a ~> a ~> b) ~> b
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> ((a ~> a) ~> a) ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> ((a ~> a) ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a ~> a ~> a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> a) ~> ((a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> a ~> b) ~> b
, prove $ a ~> (a ~> a) ~> (a ~> (a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a) ~> (a ~> a ~> a ~> b) ~> b
, prove $ (a ~> a) ~> ((((a ~> a) ~> (a ~> a) ~> b) ~> b) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (((a ~> a) ~> b) ~> b) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> (b ~> b) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> b) ~> (b ~> a) ~> a
, prove $ ((((((a ~> a) ~> a ~> a) ~> a ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ ((((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> (b ~> b) ~> c) ~> c
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> b) ~> (b ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> ((((a ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> (b ~> b) ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> b) ~> (b ~> c) ~> c
, prove $ (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> b) ~> c ~> ((a ~> a) ~> a ~> a) ~> b
, prove $ ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b) ~> c ~> ((a ~> a) ~> a ~> a) ~> b
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> b) ~> c ~> b
, prove $ ((((a ~> a) ~> a) ~> (a ~> a) ~> a) ~> b) ~> c ~> b
, prove $ (((a ~> a ~> a) ~> a ~> a ~> a) ~> b) ~> c ~> b
, prove $ (((a ~> a) ~> ((a ~> a) ~> a) ~> a) ~> b) ~> c ~> b
, prove $ ((a ~> (a ~> a ~> a) ~> a ~> a) ~> b) ~> c ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> (a ~> a) ~> b) ~> c ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> b) ~> c ~> b
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> b) ~> c ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> (a ~> b) ~> c ~> b
, prove $ (a ~> a ~> a) ~> ((a ~> a ~> a) ~> b) ~> c ~> b
, prove $ (a ~> a ~> a) ~> a ~> ((a ~> a) ~> b) ~> c ~> b
, prove $ (a ~> a) ~> ((((a ~> a) ~> a) ~> a) ~> b) ~> c ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> a) ~> b) ~> c ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> (a ~> b) ~> c ~> b
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> a ~> b) ~> c ~> b
, prove $ (a ~> a) ~> a ~> (a ~> (a ~> a) ~> b) ~> c ~> b
, prove $ a ~> (((a ~> a ~> a) ~> a ~> a) ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> a ~> a ~> a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> a) ~> ((a ~> a) ~> b) ~> c ~> b
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a) ~> (a ~> (a ~> a) ~> b) ~> c ~> b
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> b ~> c) ~> b ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> b ~> c) ~> b ~> c
, prove $ ((((a ~> a) ~> a ~> a) ~> a ~> a) ~> b) ~> c ~> d ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((a ~> a) ~> b) ~> c ~> d ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> b ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> b ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> b ~> a
, prove $ (a ~> a ~> a) ~> a ~> a ~> b ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> b ~> a
, prove $ (a ~> a) ~> (a ~> a) ~> a ~> b ~> a
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> b) ~> a
, prove $ (a ~> a) ~> a ~> (a ~> a) ~> b ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> b ~> a
, prove $ a ~> (a ~> a ~> a ~> a ~> b) ~> a
, prove $ a ~> (a ~> a ~> a) ~> a ~> b ~> a
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> b) ~> a
, prove $ a ~> (a ~> a) ~> (a ~> a) ~> b ~> a
, prove $ a ~> a ~> (a ~> a ~> a) ~> b ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> (a ~> b) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> b ~> a ~> a
, prove $ (a ~> a ~> a ~> a) ~> a ~> b ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> b ~> a ~> a
, prove $ a ~> (a ~> a ~> a ~> a) ~> b ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> b ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a ~> a) ~> b ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> b ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> b ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a ~> a) ~> a ~> b ~> a ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> b ~> (a ~> a) ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> b ~> (a ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> a) ~> b ~> a ~> a ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> a) ~> b ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> a ~> a) ~> b ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a ~> a ~> a ~> a) ~> b ~> a ~> a ~> a ~> a ~> a
, prove $ ((a ~> a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a ~> a) ~> a ~> b
, prove $ ((a ~> a ~> a) ~> (a ~> a) ~> b) ~> a ~> (a ~> a ~> a) ~> b
, prove $ ((a ~> a) ~> (a ~> a ~> a) ~> b) ~> (a ~> a ~> a) ~> a ~> b
, prove $ ((a ~> a) ~> (a ~> a ~> a) ~> b) ~> a ~> (a ~> a ~> a) ~> b
, prove $ a ~> (a ~> a ~> a ~> a ~> b) ~> a ~> a ~> a ~> a ~> b
, prove $ ((a ~> a) ~> (((a ~> a) ~> a) ~> b) ~> a) ~> (((a ~> a) ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> (((a ~> a) ~> a ~> b) ~> a) ~> ((a ~> a) ~> a ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> (a ~> a) ~> b) ~> a) ~> (a ~> (a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> a ~> b) ~> (a ~> a) ~> a ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> a ~> b) ~> a ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> (a ~> a) ~> b) ~> (a ~> a) ~> a ~> b
, prove $ ((a ~> a) ~> a ~> (a ~> a) ~> b) ~> a ~> (a ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a) ~> a ~> b
, prove $ (a ~> (a ~> a) ~> (a ~> a) ~> b) ~> a ~> (a ~> a) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> b) ~> (((a ~> a) ~> a ~> b) ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> b) ~> ((a ~> (a ~> a) ~> b) ~> a) ~> b
, prove $ a ~> ((a ~> a) ~> a ~> a ~> b) ~> (a ~> a) ~> b
, prove $ a ~> (a ~> (a ~> a) ~> a ~> b) ~> (a ~> a) ~> b
, prove $ a ~> (a ~> a ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> b) ~> a) ~> (a ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> b ~> (a ~> a) ~> c ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> a) ~> b) ~> a ~> b
, prove $ (((a ~> a ~> a) ~> a ~> a) ~> b) ~> a ~> b
, prove $ (((a ~> a) ~> a) ~> a ~> a ~> b) ~> a ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> (a ~> b) ~> a ~> b
, prove $ (a ~> ((a ~> a) ~> a) ~> a ~> b) ~> a ~> b
, prove $ (a ~> a ~> ((a ~> a) ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a ~> a ~> a ~> a ~> b) ~> a ~> b
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> b) ~> a ~> b
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a) ~> (a ~> a ~> a ~> b) ~> a ~> b
, prove $ (((a ~> a ~> a) ~> a ~> a) ~> b) ~> a ~> c ~> b
, prove $ (a ~> a ~> a ~> a ~> a ~> b) ~> a ~> c ~> b
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> b) ~> a ~> c ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> b) ~> a ~> c ~> b
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> b) ~> a ~> c ~> b
, prove $ ((((a ~> a) ~> a) ~> (a ~> a) ~> b ~> a) ~> c) ~> c
, prove $ (((a ~> a) ~> ((a ~> a) ~> a) ~> b ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> (((a ~> a) ~> b ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> ((b ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> b ~> (a ~> c) ~> c
, prove $ (a ~> a) ~> ((((a ~> a) ~> a) ~> b ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> (a ~> b ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> ((b ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> b ~> (a ~> c) ~> c
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> (b ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> a ~> (b ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> (b ~> a) ~> c) ~> c
, prove $ (((a ~> a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a ~> a ~> a) ~> b) ~> b
, prove $ ((a ~> (a ~> a ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> (a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> b ~> b
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> b) ~> b
, prove $ (a ~> a ~> a) ~> a ~> (a ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> b ~> b
, prove $ (a ~> a) ~> a ~> ((a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> a ~> (a ~> a ~> b) ~> b
, prove $ a ~> (((a ~> a ~> a) ~> a) ~> b) ~> b
, prove $ a ~> (((a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ a ~> (((a ~> a) ~> a) ~> a ~> b) ~> b
, prove $ a ~> (a ~> ((a ~> a) ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a ~> a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> a) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> a) ~> ((a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a) ~> (a ~> a ~> b) ~> b
, prove $ ((a ~> (a ~> a ~> a ~> a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (((a ~> a ~> a ~> a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (a ~> ((a ~> a ~> a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> ((a ~> a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> ((a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> a ~> (b ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> a ~> b) ~> (b ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> a ~> b ~> c ~> a
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> b ~> c ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> b ~> c ~> a
, prove $ a ~> ((a ~> a) ~> a ~> a) ~> b ~> c ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> a) ~> b ~> c ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a ~> a) ~> a ~> b ~> c ~> a ~> a ~> a
, prove $ a ~> (a ~> a ~> a ~> a) ~> b ~> c ~> a ~> a ~> a
, prove $ (((a ~> a ~> a) ~> a ~> a) ~> b) ~> c ~> a ~> b
, prove $ (a ~> a ~> a ~> a ~> a ~> b) ~> c ~> a ~> b
, prove $ (a ~> a ~> a) ~> ((a ~> a) ~> b) ~> c ~> a ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> a ~> b) ~> c ~> a ~> b
, prove $ (a ~> a) ~> (a ~> (a ~> a) ~> b) ~> c ~> a ~> b
, prove $ (a ~> a) ~> a ~> (a ~> a ~> b) ~> c ~> b
, prove $ a ~> (((a ~> a) ~> a) ~> a ~> b) ~> c ~> b
, prove $ a ~> (a ~> ((a ~> a) ~> a) ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> a ~> a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a) ~> (a ~> a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> a ~> a ~> b ~> c) ~> b ~> c
, prove $ ((a ~> a) ~> a) ~> (a ~> a) ~> b ~> c ~> d ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> a) ~> b ~> c ~> d ~> a
, prove $ a ~> (a ~> a ~> a ~> a ~> b) ~> c ~> d ~> b
, prove $ (a ~> a ~> a) ~> a ~> b ~> a
, prove $ (a ~> a) ~> a ~> (a ~> b) ~> a
, prove $ a ~> (((a ~> a) ~> a) ~> b) ~> a
, prove $ a ~> (a ~> a ~> a ~> b) ~> a
, prove $ a ~> (a ~> a ~> a) ~> b ~> a
, prove $ a ~> (a ~> a) ~> (a ~> b) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> a ~> a
, prove $ (a ~> a ~> a ~> a ~> b) ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> b ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> a ~> a
, prove $ (a ~> a) ~> (a ~> a) ~> b ~> a ~> a
, prove $ (a ~> a) ~> a ~> (a ~> b) ~> a ~> a
, prove $ a ~> (a ~> a ~> a) ~> b ~> a ~> a
, prove $ a ~> (a ~> a) ~> (a ~> b) ~> a ~> a
, prove $ (a ~> a ~> a ~> a) ~> b ~> a ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> b ~> a ~> a ~> a
, prove $ a ~> (a ~> a ~> a) ~> b ~> a ~> a ~> a
, prove $ (((a ~> a) ~> a) ~> a) ~> b ~> ((a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> (a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> a ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a ~> a) ~> b ~> a ~> a ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> a ~> a) ~> a) ~> a
, prove $ ((a ~> a ~> a) ~> a) ~> b ~> (a ~> a ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a ~> a) ~> b) ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> (b ~> a ~> a) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> (a ~> a) ~> a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> (((a ~> a) ~> a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> ((a ~> a) ~> a ~> a) ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> a ~> a) ~> (a ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a ~> a) ~> b ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> b ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> (a ~> a) ~> a ~> a) ~> (a ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> a ~> a) ~> ((a ~> a) ~> a ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> (((a ~> a) ~> a ~> a) ~> (a ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> ((a ~> a) ~> ((a ~> a) ~> a ~> a) ~> c) ~> c
, prove $ (((a ~> a) ~> a) ~> a ~> b) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> b
, prove $ (((a ~> a) ~> a) ~> a ~> b) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> b
, prove $ (a ~> ((a ~> a) ~> a) ~> b) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> b
, prove $ (a ~> ((a ~> a) ~> a) ~> b) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> b
, prove $ (a ~> a ~> a ~> a ~> b) ~> a ~> a ~> a ~> a ~> a ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> b) ~> ((a ~> a) ~> a ~> a) ~> b
, prove $ ((a ~> (a ~> a) ~> a) ~> b) ~> (a ~> (a ~> a) ~> a) ~> b
, prove $ ((a ~> a ~> a ~> a) ~> b) ~> (a ~> a ~> a ~> a) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a) ~> (a ~> a) ~> b
, prove $ (a ~> a ~> a ~> a ~> b) ~> a ~> a ~> a ~> a ~> b
, prove $ a ~> ((a ~> a ~> a) ~> b) ~> (a ~> a ~> a ~> a) ~> b
, prove $ a ~> (a ~> a ~> a ~> (b ~> a) ~> a) ~> a ~> a ~> (b ~> a) ~> a
, prove $ ((a ~> a) ~> ((a ~> a) ~> b) ~> a ~> a) ~> ((a ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a) ~> a ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> a ~> b) ~> (a ~> a) ~> a ~> b
, prove $ ((a ~> a) ~> a ~> a ~> b) ~> a ~> (a ~> a) ~> b
, prove $ (a ~> ((a ~> a) ~> a) ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> a ~> b) ~> (a ~> a) ~> a ~> b
, prove $ (a ~> (a ~> a) ~> a ~> b) ~> a ~> (a ~> a) ~> b
, prove $ (a ~> a ~> (a ~> a) ~> b) ~> (a ~> a) ~> a ~> b
, prove $ (a ~> a ~> (a ~> a) ~> b) ~> a ~> (a ~> a) ~> b
, prove $ a ~> (((a ~> a) ~> a) ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ a ~> ((a ~> a) ~> a ~> b) ~> (a ~> a ~> a) ~> b
, prove $ a ~> (a ~> (a ~> a) ~> b) ~> (a ~> a ~> a) ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> a ~> a ~> a ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> b ~> a) ~> (a ~> a) ~> b ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> (a ~> a) ~> a) ~> b ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> a) ~> ((a ~> a) ~> b) ~> a
, prove $ a ~> ((a ~> a ~> a ~> b) ~> a ~> a ~> a ~> b) ~> (a ~> a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> ((a ~> a ~> a ~> b) ~> a ~> a ~> a ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> a) ~> (((a ~> a) ~> b ~> a) ~> b) ~> a
, prove $ a ~> (a ~> a ~> a ~> b) ~> ((a ~> a ~> a ~> b) ~> b ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> a ~> a) ~> a) ~> c ~> a
, prove $ ((((a ~> a) ~> a) ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> b) ~> (a ~> a) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ a ~> ((a ~> a) ~> a ~> b) ~> (a ~> a) ~> b
, prove $ a ~> (a ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> (a ~> a) ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> a ~> a ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a) ~> (b ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> ((a ~> a) ~> b ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> a ~> a) ~> b ~> a ~> a) ~> b ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> a ~> a) ~> b ~> a ~> a) ~> b ~> a ~> a
, prove $ a ~> (a ~> a ~> a ~> b) ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> ((a ~> a ~> b) ~> a) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> (((a ~> a) ~> b) ~> b ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> ((a ~> a) ~> b ~> c) ~> c
, prove $ (((a ~> a) ~> a ~> a) ~> (b ~> a ~> a) ~> c) ~> ((a ~> a) ~> a ~> a) ~> c
, prove $ ((((a ~> a) ~> a) ~> a) ~> b) ~> (a ~> a) ~> c ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> (a ~> a) ~> c ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> b) ~> (a ~> a) ~> c ~> b
, prove $ a ~> ((a ~> a) ~> a ~> b) ~> (a ~> a) ~> c ~> b
, prove $ a ~> (a ~> (a ~> a) ~> b) ~> (a ~> a) ~> c ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> (b ~> (a ~> a) ~> c) ~> b ~> c
, prove $ ((((a ~> a) ~> a ~> a) ~> b ~> a ~> a) ~> c) ~> c
, prove $ (((a ~> a ~> a) ~> a ~> b ~> a ~> a) ~> c) ~> c
, prove $ ((a ~> (a ~> a ~> a) ~> b ~> a ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> (a ~> a) ~> (b ~> a ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> a ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> ((a ~> a) ~> c) ~> c
, prove $ (a ~> a ~> a) ~> ((a ~> b ~> a ~> a) ~> c) ~> c
, prove $ (a ~> a ~> a) ~> a ~> ((b ~> a ~> a) ~> c) ~> c
, prove $ (a ~> a ~> a) ~> a ~> b ~> ((a ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> a ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> a ~> (a ~> (b ~> a ~> a) ~> c) ~> c
, prove $ a ~> (((a ~> a ~> a) ~> b ~> a ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> (b ~> a) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> a) ~> ((b ~> a ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a ~> a) ~> b ~> ((a ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a) ~> (a ~> (b ~> a ~> a) ~> c) ~> c
, prove $ ((((a ~> a) ~> a ~> a) ~> b ~> a ~> a) ~> c) ~> d ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> a ~> a) ~> c) ~> d ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> ((a ~> a) ~> c) ~> d ~> c
, prove $ (((a ~> a ~> a) ~> a) ~> b) ~> a ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> b) ~> a ~> b
, prove $ (((a ~> a) ~> a) ~> a ~> b) ~> a ~> b
, prove $ (a ~> ((a ~> a) ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a ~> a ~> a ~> b) ~> a ~> b
, prove $ (a ~> a ~> a) ~> (a ~> b) ~> a ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a) ~> (a ~> a ~> b) ~> a ~> b
, prove $ (a ~> a) ~> a ~> (a ~> b) ~> a ~> b
, prove $ a ~> (a ~> a) ~> (a ~> b) ~> a ~> b
, prove $ a ~> a ~> (a ~> a ~> b) ~> a ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> (b ~> a) ~> b ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> a) ~> b ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> b ~> a) ~> b ~> (a ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> b ~> a) ~> b ~> a ~> a ~> b ~> a
, prove $ (a ~> a) ~> (((a ~> a) ~> b ~> a) ~> b) ~> ((a ~> a) ~> b ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> b) ~> ((a ~> b) ~> a ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> a) ~> b) ~> (b ~> a) ~> a
, prove $ (a ~> a ~> a ~> a ~> b) ~> ((a ~> b) ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> a) ~> b ~> c ~> a
, prove $ (((a ~> a ~> a ~> a ~> b) ~> a ~> b) ~> c) ~> c
, prove $ (a ~> a ~> a ~> a ~> b) ~> ((a ~> b) ~> c) ~> c
, prove $ (a ~> a ~> a ~> a ~> b) ~> a ~> (b ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> b) ~> (a ~> b ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> a ~> c ~> a
, prove $ (a ~> a ~> a ~> a) ~> b ~> a ~> c ~> a ~> a ~> a
, prove $ (a ~> a ~> a ~> a ~> (b ~> a) ~> c) ~> a ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> a) ~> c) ~> a ~> c
, prove $ (((a ~> a) ~> a) ~> a ~> b) ~> a ~> c ~> b
, prove $ (a ~> ((a ~> a) ~> a) ~> b) ~> a ~> c ~> b
, prove $ (a ~> a ~> a ~> a ~> b) ~> a ~> c ~> b
, prove $ (a ~> a) ~> (a ~> a ~> b) ~> a ~> c ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> a) ~> c ~> b ~> a
, prove $ a ~> (a ~> a ~> a ~> b ~> a ~> c) ~> b ~> c
, prove $ (a ~> a) ~> a ~> (a ~> (b ~> a) ~> c) ~> c
, prove $ a ~> (((a ~> a) ~> a) ~> (b ~> a) ~> c) ~> c
, prove $ a ~> (a ~> ((a ~> a) ~> b ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> (b ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a) ~> (a ~> (b ~> a) ~> c) ~> c
, prove $ (a ~> a ~> a ~> a ~> b) ~> a ~> c ~> d ~> b
, prove $ a ~> (a ~> a ~> a ~> (b ~> a) ~> c) ~> d ~> c
, prove $ ((((a ~> a) ~> a) ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> b) ~> b
, prove $ ((a ~> (a ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> b) ~> b
, prove $ (a ~> a ~> a) ~> a ~> b ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> b
, prove $ (a ~> a) ~> a ~> (a ~> b) ~> b
, prove $ a ~> (((a ~> a) ~> a) ~> b) ~> b
, prove $ a ~> ((a ~> a) ~> a ~> b) ~> b
, prove $ a ~> (a ~> (a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> a) ~> b ~> b
, prove $ a ~> (a ~> a) ~> (a ~> b) ~> b
, prove $ a ~> a ~> (a ~> a ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> b) ~> a) ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> (b ~> a) ~> a
, prove $ (a ~> a) ~> ((((a ~> a) ~> b) ~> b) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> b) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> (b ~> a) ~> a
, prove $ ((((a ~> a) ~> (a ~> a) ~> b) ~> b) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> (((a ~> a) ~> b) ~> b) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> (b ~> b) ~> a) ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> (b ~> a) ~> (a ~> a) ~> a
, prove $ (a ~> a) ~> ((((a ~> a) ~> b) ~> b) ~> (a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> b) ~> (a ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> (b ~> (a ~> a) ~> a) ~> a
, prove $ ((a ~> (a ~> a ~> a ~> b) ~> b) ~> a ~> (a ~> a ~> a ~> b) ~> b) ~> a ~> (a ~> a ~> a ~> b) ~> b
, prove $ (((a ~> a) ~> ((a ~> a) ~> b) ~> b) ~> (a ~> a) ~> ((a ~> a) ~> b) ~> b) ~> ((a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> (b ~> a) ~> a ~> a ~> b
, prove $ (a ~> a) ~> (((a ~> a) ~> b) ~> b ~> a) ~> ((a ~> a) ~> b) ~> a
, prove $ a ~> (a ~> ((a ~> a ~> b) ~> b) ~> a) ~> ((a ~> a ~> b) ~> b) ~> a
, prove $ a ~> (a ~> a ~> ((a ~> b) ~> b) ~> a) ~> a ~> ((a ~> b) ~> b) ~> a
, prove $ a ~> (a ~> a ~> a ~> (b ~> b) ~> a) ~> a ~> a ~> (b ~> b) ~> a
, prove $ a ~> (((a ~> a ~> a ~> b) ~> b) ~> (a ~> a ~> a ~> b) ~> b) ~> (a ~> a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> (b ~> (a ~> a ~> a ~> b) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> (b ~> ((a ~> a) ~> b) ~> a) ~> a
, prove $ ((a ~> a) ~> ((a ~> a) ~> b) ~> b) ~> ((a ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> b) ~> (a ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> (b ~> (a ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> b ~> a) ~> b ~> a
, prove $ (a ~> a) ~> ((((a ~> a) ~> b) ~> b) ~> a) ~> c ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> b) ~> a) ~> c ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> (b ~> a) ~> c ~> a
, prove $ a ~> (((a ~> a ~> a ~> b) ~> b) ~> a ~> c) ~> c
, prove $ a ~> (a ~> ((a ~> a ~> b) ~> b) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> ((a ~> b) ~> b) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> (b ~> b) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> b) ~> (b ~> a ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> b) ~> b ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> (b ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> b) ~> b ~> b) ~> b ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> (b ~> b ~> c) ~> c
, prove $ a ~> ((a ~> a ~> a ~> b) ~> b ~> c) ~> (a ~> a ~> a ~> b) ~> c
, prove $ a ~> (a ~> (a ~> a ~> b) ~> b ~> c) ~> (a ~> a ~> b) ~> c
, prove $ a ~> (a ~> a ~> (a ~> b) ~> b ~> c) ~> (a ~> b) ~> c
, prove $ (((a ~> a ~> a ~> a ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (a ~> ((a ~> a ~> a ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (a ~> a ~> ((a ~> a ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> ((a ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> a ~> (b ~> b) ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> a ~> b) ~> (b ~> c) ~> a ~> c
, prove $ a ~> (a ~> a ~> a ~> b ~> b ~> c) ~> b ~> c
, prove $ (((((a ~> a) ~> a ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ ((((a ~> (a ~> a) ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ ((((a ~> a) ~> (a ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ (((a ~> a) ~> ((a ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ (((a ~> a) ~> a ~> (a ~> b) ~> b) ~> c) ~> c
, prove $ (((a ~> a) ~> a ~> a) ~> (b ~> b) ~> c) ~> c
, prove $ (((a ~> a) ~> a ~> a) ~> b) ~> (b ~> c) ~> c
, prove $ ((a ~> (((a ~> a) ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ ((a ~> (a ~> a ~> a ~> b) ~> b) ~> c) ~> c
, prove $ ((a ~> (a ~> a) ~> (a ~> b) ~> b) ~> c) ~> c
, prove $ ((a ~> (a ~> a) ~> a) ~> (b ~> b) ~> c) ~> c
, prove $ ((a ~> (a ~> a) ~> a) ~> b) ~> (b ~> c) ~> c
, prove $ ((a ~> a) ~> (((a ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ ((a ~> a) ~> (a ~> a) ~> (b ~> b) ~> c) ~> c
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> (b ~> c) ~> c
, prove $ (a ~> a) ~> ((((a ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> (a ~> b) ~> b) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> b) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> (b ~> c) ~> c
, prove $ (a ~> a) ~> a ~> (((a ~> b) ~> b) ~> c) ~> c
, prove $ (a ~> a) ~> a ~> (a ~> (b ~> b) ~> c) ~> c
, prove $ (a ~> a) ~> a ~> (a ~> b) ~> (b ~> c) ~> c
, prove $ a ~> (((((a ~> a) ~> a) ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (((a ~> a ~> a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (((a ~> a) ~> (a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (((a ~> a) ~> a) ~> (b ~> b) ~> c) ~> c
, prove $ a ~> (((a ~> a) ~> a) ~> b) ~> (b ~> c) ~> c
, prove $ a ~> (a ~> ((a ~> a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> ((a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> (b ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> a ~> b) ~> (b ~> c) ~> c
, prove $ a ~> (a ~> a) ~> (((a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a) ~> (a ~> (b ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a) ~> (a ~> b) ~> (b ~> c) ~> c
, prove $ ((a ~> (a ~> a ~> a ~> b) ~> b) ~> c) ~> d ~> c
, prove $ a ~> (((a ~> a ~> a ~> b) ~> b) ~> c) ~> d ~> c
, prove $ a ~> (a ~> ((a ~> a ~> b) ~> b) ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> ((a ~> b) ~> b) ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> a ~> (b ~> b) ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> a ~> b) ~> (b ~> c) ~> d ~> c
, prove $ (a ~> a ~> a) ~> a ~> b ~> c ~> a
, prove $ a ~> (a ~> a ~> a ~> b) ~> c ~> a
, prove $ a ~> (a ~> a ~> a) ~> b ~> c ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> c ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> b ~> c ~> a ~> a
, prove $ a ~> (a ~> a ~> a) ~> b ~> c ~> a ~> a
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> c ~> (a ~> a) ~> a ~> a
, prove $ (a ~> a ~> a ~> a) ~> b ~> c ~> a ~> a ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> c ~> a ~> a) ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> b) ~> c ~> a ~> a ~> a ~> b
, prove $ a ~> (a ~> a ~> a ~> b ~> c) ~> ((a ~> a ~> a ~> b ~> c) ~> b) ~> c
, prove $ ((((a ~> a) ~> a) ~> a) ~> b) ~> c ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> c ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> b) ~> c ~> (a ~> a) ~> b
, prove $ a ~> ((a ~> a) ~> a ~> b) ~> c ~> (a ~> a) ~> b
, prove $ a ~> (a ~> (a ~> a) ~> b) ~> c ~> (a ~> a) ~> b
, prove $ ((((a ~> a) ~> a ~> a) ~> b) ~> c) ~> ((a ~> a) ~> b) ~> c
, prove $ ((a ~> a) ~> a ~> a) ~> (b ~> c) ~> ((a ~> a) ~> b) ~> c
, prove $ ((a ~> a) ~> ((a ~> a) ~> b) ~> c) ~> ((((a ~> a) ~> b) ~> c) ~> b) ~> c
, prove $ ((((a ~> a) ~> a ~> a) ~> b ~> c ~> a ~> a) ~> d) ~> d
, prove $ ((a ~> a) ~> a ~> a) ~> ((b ~> c ~> a ~> a) ~> d) ~> d
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> ((c ~> a ~> a) ~> d) ~> d
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> c ~> ((a ~> a) ~> d) ~> d
, prove $ (((a ~> a) ~> a) ~> a ~> b) ~> c ~> a ~> b
, prove $ (a ~> ((a ~> a) ~> a) ~> b) ~> c ~> a ~> b
, prove $ (a ~> a ~> a ~> a ~> b) ~> c ~> a ~> b
, prove $ (a ~> a) ~> (a ~> a ~> b) ~> c ~> a ~> b
, prove $ (a ~> a ~> a ~> a ~> b ~> c) ~> a ~> b ~> c
, prove $ a ~> (a ~> a ~> a ~> b ~> c) ~> (a ~> b) ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> c) ~> a) ~> c ~> a
, prove $ (a ~> a ~> a ~> a ~> b) ~> c ~> a ~> d ~> b
, prove $ a ~> (a ~> a ~> a ~> (b ~> c ~> a) ~> d) ~> d
, prove $ ((((a ~> a) ~> a) ~> a) ~> b) ~> c ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> b) ~> c ~> b
, prove $ ((a ~> (a ~> a) ~> a) ~> b) ~> c ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> c ~> b
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> c ~> b
, prove $ ((a ~> a) ~> a) ~> (a ~> b) ~> c ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> c ~> b
, prove $ (a ~> a) ~> a ~> (a ~> b) ~> c ~> b
, prove $ a ~> (((a ~> a) ~> a) ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a) ~> (a ~> b) ~> c ~> b
, prove $ (a ~> a) ~> ((((a ~> a) ~> b) ~> c ~> b) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> c ~> b) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> ((c ~> b) ~> a) ~> a
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> c ~> (b ~> a) ~> a
, prove $ a ~> ((a ~> a ~> a ~> b ~> c) ~> b) ~> (a ~> a ~> a ~> b ~> c) ~> c
, prove $ a ~> (a ~> (a ~> a ~> b ~> c) ~> b) ~> (a ~> a ~> b ~> c) ~> c
, prove $ (a ~> a ~> a ~> ((a ~> b) ~> c) ~> b) ~> ((a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> (a ~> b ~> c) ~> b) ~> (a ~> b ~> c) ~> c
, prove $ (a ~> a ~> a ~> a ~> b ~> c) ~> b ~> a ~> c
, prove $ a ~> (a ~> a ~> a ~> (b ~> c) ~> b) ~> (b ~> c) ~> c
, prove $ (((a ~> a) ~> a ~> a) ~> b ~> c) ~> b ~> c
, prove $ ((a ~> (a ~> a) ~> a) ~> b ~> c) ~> b ~> c
, prove $ ((a ~> a) ~> (a ~> a) ~> b ~> c) ~> b ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> c) ~> b ~> c
, prove $ (a ~> a) ~> a ~> (a ~> b ~> c) ~> b ~> c
, prove $ a ~> (((a ~> a) ~> a) ~> b ~> c) ~> b ~> c
, prove $ a ~> (a ~> a ~> a ~> b ~> c) ~> b ~> c
, prove $ a ~> (a ~> a) ~> (a ~> b ~> c) ~> b ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> b ~> c) ~> ((b ~> c) ~> b) ~> c
, prove $ a ~> (a ~> a ~> a ~> b ~> c) ~> b ~> d ~> c
, prove $ ((a ~> (a ~> a ~> a ~> b) ~> c ~> b) ~> d) ~> d
, prove $ a ~> (((a ~> a ~> a ~> b) ~> c ~> b) ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> a ~> b) ~> c ~> b) ~> d) ~> d
, prove $ a ~> (a ~> a ~> ((a ~> b) ~> c ~> b) ~> d) ~> d
, prove $ a ~> (a ~> a ~> a ~> (b ~> c ~> b) ~> d) ~> d
, prove $ a ~> (a ~> a ~> a ~> b) ~> ((c ~> b) ~> d) ~> d
, prove $ a ~> (a ~> a ~> a ~> b) ~> c ~> (b ~> d) ~> d
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> c ~> c
, prove $ a ~> (a ~> a ~> a ~> b) ~> c ~> c
, prove $ (a ~> a) ~> ((a ~> a) ~> (b ~> c ~> c) ~> a) ~> a
, prove $ a ~> (a ~> a ~> a ~> (b ~> c ~> c) ~> d) ~> d
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> c ~> d ~> a ~> a
, prove $ (a ~> a ~> a) ~> a ~> b ~> c ~> d ~> a ~> a
, prove $ a ~> (a ~> a ~> a) ~> b ~> c ~> d ~> a ~> a
, prove $ (a ~> a ~> a ~> a ~> b) ~> c ~> d ~> a ~> b
, prove $ (((a ~> a) ~> a ~> a) ~> b) ~> c ~> d ~> b
, prove $ ((a ~> (a ~> a) ~> a) ~> b) ~> c ~> d ~> b
, prove $ ((a ~> a) ~> (a ~> a) ~> b) ~> c ~> d ~> b
, prove $ (a ~> a) ~> ((a ~> a) ~> b) ~> c ~> d ~> b
, prove $ (a ~> a) ~> a ~> (a ~> b) ~> c ~> d ~> b
, prove $ a ~> (((a ~> a) ~> a) ~> b) ~> c ~> d ~> b
, prove $ a ~> (a ~> a ~> a ~> b) ~> c ~> d ~> b
, prove $ a ~> (a ~> a) ~> (a ~> b) ~> c ~> d ~> b
, prove $ a ~> (a ~> a ~> a ~> b ~> c) ~> d ~> b ~> c
, prove $ a ~> (a ~> a ~> a ~> (b ~> c) ~> d) ~> c ~> d
, prove $ ((a ~> a) ~> a ~> a) ~> b ~> c ~> d ~> e ~> a ~> a
, prove $ a ~> (a ~> a ~> a ~> b) ~> c ~> d ~> e ~> b
, prove $ ((a ~> a) ~> a) ~> b ~> a
, prove $ (a ~> a) ~> a ~> b ~> a
, prove $ a ~> (a ~> a ~> b) ~> a
, prove $ a ~> (a ~> a) ~> b ~> a
, prove $ (((a ~> a) ~> a) ~> b) ~> a ~> a
, prove $ (a ~> a ~> a ~> b) ~> a ~> a
, prove $ (a ~> a ~> a) ~> b ~> a ~> a
, prove $ (a ~> a) ~> (a ~> b) ~> a ~> a
, prove $ (a ~> a) ~> a ~> b ~> a ~> a
, prove $ a ~> (a ~> a) ~> b ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a) ~> b ~> a ~> a ~> a
, prove $ (a ~> a) ~> ((a ~> b ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> (a ~> b) ~> a ~> a ~> a
, prove $ (a ~> a) ~> a ~> ((b ~> a) ~> a) ~> a
, prove $ (a ~> a) ~> a ~> b ~> (a ~> a) ~> a
, prove $ a ~> ((a ~> a) ~> b) ~> (a ~> a) ~> a
, prove $ a ~> (a ~> a) ~> ((b ~> a) ~> a) ~> a
, prove $ a ~> (a ~> a) ~> b ~> (a ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> a) ~> a ~> a
, prove $ (a ~> a ~> a) ~> b ~> a ~> a ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> b ~> (((a ~> a) ~> a) ~> a) ~> a
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> a ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> a) ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a) ~> b ~> ((a ~> a) ~> a) ~> a ~> a
, prove $ (a ~> a) ~> a ~> b ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ a ~> (a ~> a) ~> b ~> ((a ~> a) ~> a ~> a) ~> a
, prove $ (a ~> a ~> a) ~> b ~> ((a ~> a ~> a) ~> a) ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> b ~> (((a ~> a) ~> a) ~> a ~> a) ~> a ~> a
, prove $ ((((a ~> a) ~> a) ~> b) ~> (a ~> a) ~> a) ~> (((a ~> a) ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a ~> b) ~> a) ~> (a ~> a) ~> ((a ~> a) ~> a ~> b) ~> b
, prove $ ((a ~> (a ~> a) ~> b) ~> a) ~> (a ~> a) ~> (a ~> (a ~> a) ~> b) ~> b
, prove $ (((a ~> a) ~> a) ~> b) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> b
, prove $ ((a ~> a ~> a) ~> b) ~> (a ~> a ~> a ~> a) ~> a ~> b
, prove $ ((a ~> a ~> a) ~> b) ~> a ~> (a ~> a ~> a ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> ((a ~> a) ~> a) ~> (a ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> (a ~> a) ~> ((a ~> a) ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> ((a ~> a) ~> (a ~> a) ~> a) ~> b
, prove $ (a ~> a ~> a ~> (b ~> a) ~> a) ~> a ~> a ~> a ~> (b ~> a) ~> a
, prove $ (((a ~> a) ~> a) ~> b) ~> ((a ~> a) ~> (((a ~> a) ~> a) ~> b) ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> (a ~> a) ~> (((a ~> a) ~> a ~> b) ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> (a ~> a) ~> ((a ~> (a ~> a) ~> b) ~> a) ~> b
, prove $ (((a ~> a) ~> a) ~> b) ~> a ~> ((a ~> a) ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> (a ~> a ~> a) ~> a ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> a ~> (a ~> a ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> (a ~> a ~> a) ~> a ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> a ~> (a ~> a ~> a) ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> a ~> a ~> a ~> b
, prove $ a ~> (a ~> a ~> (b ~> a) ~> a ~> a) ~> a ~> (b ~> a) ~> a ~> a
, prove $ (((a ~> a) ~> a ~> b ~> a) ~> (a ~> a) ~> a ~> b ~> a) ~> (a ~> a) ~> a ~> b ~> a
, prove $ ((a ~> (a ~> a) ~> b ~> a) ~> a ~> (a ~> a) ~> b ~> a) ~> a ~> (a ~> a) ~> b ~> a
, prove $ (a ~> a ~> a ~> b) ~> a ~> ((a ~> a ~> a ~> b) ~> a ~> a ~> a ~> b) ~> b
, prove $ (((a ~> a) ~> a ~> b) ~> a) ~> ((a ~> a) ~> a ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> (a ~> a) ~> b) ~> a) ~> (a ~> (a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ ((((a ~> a) ~> a) ~> b) ~> a) ~> (((a ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> a ~> a ~> b) ~> a) ~> (a ~> a ~> a ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> b) ~> a) ~> (a ~> a) ~> (a ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> b) ~> (a ~> a) ~> a) ~> (a ~> b) ~> b
, prove $ a ~> ((a ~> a ~> b) ~> a) ~> (a ~> a ~> a ~> b) ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> ((a ~> a ~> a ~> b) ~> b ~> c) ~> c
, prove $ ((((a ~> a) ~> a) ~> b) ~> a) ~> (((a ~> a) ~> a) ~> b) ~> c ~> b
, prove $ (((a ~> a) ~> a) ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ ((a ~> a ~> a) ~> b) ~> (a ~> a ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> (a ~> a) ~> a ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> a ~> (a ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> (a ~> a) ~> a ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> a ~> (a ~> a) ~> b
, prove $ (a ~> a ~> a ~> b) ~> (a ~> a) ~> a ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> (a ~> a) ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> a ~> a ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> ((a ~> a) ~> a) ~> b
, prove $ a ~> ((a ~> a) ~> b) ~> (a ~> a ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> (b ~> a) ~> a) ~> a ~> (b ~> a) ~> a
, prove $ a ~> (a ~> a ~> (b ~> a) ~> a) ~> a ~> (b ~> a) ~> a
, prove $ ((((a ~> a) ~> a) ~> b) ~> (((a ~> a) ~> a) ~> b) ~> a) ~> (((a ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> a ~> a ~> b) ~> a ~> a ~> a ~> b) ~> a ~> (a ~> a ~> a ~> b) ~> b
, prove $ (((a ~> a) ~> a) ~> b) ~> ((((a ~> a) ~> a) ~> b) ~> (a ~> a) ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> (((a ~> a) ~> a ~> b) ~> a) ~> (a ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> ((a ~> (a ~> a) ~> b) ~> a) ~> (a ~> a) ~> b
, prove $ a ~> (((a ~> a) ~> b ~> a) ~> (a ~> a) ~> b ~> a) ~> (a ~> a) ~> b ~> a
, prove $ (((a ~> a) ~> a) ~> b) ~> ((((a ~> a) ~> a) ~> b) ~> (((a ~> a) ~> a) ~> b) ~> a) ~> b
, prove $ ((a ~> a ~> a ~> b) ~> a ~> a ~> a ~> b) ~> (a ~> a ~> a ~> b) ~> a ~> b
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> a ~> a ~> b) ~> a ~> a ~> a ~> b) ~> a ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> b
, prove $ (((a ~> a) ~> a) ~> b) ~> ((((a ~> a) ~> a) ~> b) ~> a) ~> b
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> a ~> a ~> b) ~> a) ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> ((a ~> a ~> b) ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> ((a ~> a) ~> (a ~> b) ~> a) ~> b
, prove $ a ~> (a ~> a ~> b ~> a) ~> ((a ~> a ~> b ~> a) ~> b) ~> a ~> b ~> a
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> a ~> a ~> b) ~> (a ~> b) ~> c) ~> c
, prove $ (((a ~> a) ~> a) ~> b) ~> ((((a ~> a) ~> a) ~> b) ~> a) ~> c ~> b
, prove $ (a ~> ((a ~> a) ~> b) ~> a) ~> ((a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> (a ~> b) ~> a) ~> (a ~> a ~> b) ~> b
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> a ~> a ~> b) ~> b ~> c) ~> a ~> c
, prove $ a ~> (a ~> a ~> b) ~> (a ~> (a ~> a ~> b) ~> b ~> c) ~> c
, prove $ (((a ~> a) ~> a) ~> b) ~> ((a ~> a) ~> a) ~> c ~> b
, prove $ ((a ~> a ~> a) ~> b) ~> (a ~> a ~> a) ~> c ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> (a ~> a) ~> a ~> c ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> a ~> (a ~> a) ~> c ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> (a ~> a) ~> a ~> c ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> a ~> (a ~> a) ~> c ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> ((a ~> a) ~> a) ~> c ~> b
, prove $ a ~> ((a ~> a) ~> b) ~> (a ~> a ~> a) ~> c ~> b
, prove $ ((((a ~> a) ~> a) ~> b ~> (a ~> a) ~> a) ~> c) ~> c
, prove $ (((a ~> a ~> a) ~> b ~> a ~> a ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> ((b ~> (a ~> a) ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> b ~> (((a ~> a) ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> a) ~> (a ~> c) ~> c
, prove $ (a ~> a ~> a) ~> ((b ~> a ~> a ~> a) ~> c) ~> c
, prove $ (a ~> a ~> a) ~> b ~> ((a ~> a ~> a) ~> c) ~> c
, prove $ (a ~> a ~> a) ~> b ~> a ~> ((a ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> b ~> a) ~> (a ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> a ~> ((b ~> a ~> a) ~> a ~> c) ~> c
, prove $ (a ~> a) ~> a ~> ((b ~> a) ~> (a ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> a ~> b ~> ((a ~> a) ~> a ~> c) ~> c
, prove $ (a ~> a) ~> a ~> b ~> (a ~> (a ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a ~> (b ~> a) ~> a ~> a ~> c) ~> c
, prove $ a ~> (a ~> a) ~> ((b ~> a ~> a) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a) ~> ((b ~> a) ~> (a ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a) ~> b ~> ((a ~> a) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a) ~> b ~> (a ~> (a ~> a) ~> c) ~> c
, prove $ ((a ~> a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> a ~> a ~> b
, prove $ a ~> ((a ~> a) ~> b) ~> (a ~> a) ~> b
, prove $ a ~> (a ~> a ~> b) ~> (a ~> a) ~> b
, prove $ a ~> (a ~> a ~> b) ~> a ~> a ~> b
, prove $ a ~> (a ~> a ~> (b ~> a) ~> a) ~> (b ~> a) ~> a
, prove $ a ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> (a ~> a ~> a ~> b) ~> b
, prove $ ((a ~> a) ~> (a ~> b) ~> a) ~> (a ~> b) ~> (a ~> a) ~> b
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> a ~> b) ~> a) ~> a ~> b
, prove $ (a ~> a ~> a ~> b ~> a) ~> a ~> b ~> a ~> a ~> b ~> a
, prove $ (a ~> a) ~> ((a ~> b ~> a) ~> a ~> b ~> a) ~> a ~> b ~> a
, prove $ a ~> (((a ~> a ~> b) ~> a ~> a ~> b) ~> a ~> a ~> b) ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> b
, prove $ a ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> (((a ~> a ~> b) ~> a ~> a ~> b) ~> a ~> a ~> b) ~> b
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> a ~> b
, prove $ a ~> (((a ~> a ~> b) ~> a ~> a ~> b) ~> a ~> a ~> b) ~> b
, prove $ a ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> (a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> (a ~> a ~> b) ~> b ~> c) ~> c
, prove $ a ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> (a ~> a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> b) ~> (a ~> (a ~> b) ~> a) ~> b
, prove $ a ~> (a ~> a ~> b ~> a) ~> (a ~> b) ~> a ~> b ~> a
, prove $ a ~> (a ~> a ~> b ~> a ~> a) ~> b ~> a ~> b ~> a ~> a
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> (a ~> b) ~> a) ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> ((a ~> b) ~> a ~> b) ~> b
, prove $ a ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> a ~> b ~> c) ~> c
, prove $ (a ~> a) ~> ((a ~> b) ~> a) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> (a ~> b) ~> a) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b ~> a) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> b ~> a) ~> a ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> b ~> a ~> a ~> b) ~> b ~> a ~> a ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> b ~> (a ~> a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> b ~> a ~> c) ~> c
, prove $ a ~> ((a ~> a ~> b) ~> (a ~> a ~> b) ~> b ~> c) ~> (a ~> a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> b ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> b ~> c) ~> d ~> c
, prove $ a ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> c ~> (a ~> a ~> b) ~> b
, prove $ (a ~> a) ~> ((a ~> b) ~> a) ~> (a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> c) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> (c ~> b) ~> d) ~> d
, prove $ ((a ~> (a ~> a ~> b) ~> a ~> a ~> b) ~> c) ~> c
, prove $ (a ~> a ~> a ~> b) ~> a ~> (a ~> b ~> c) ~> c
, prove $ a ~> (((a ~> a ~> b) ~> a ~> a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (a ~> a ~> b ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> a) ~> c ~> a
, prove $ ((a ~> a) ~> a ~> b) ~> (a ~> a) ~> c ~> a ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> (a ~> a) ~> c ~> a ~> b
, prove $ a ~> (a ~> a ~> (b ~> a) ~> a) ~> c ~> a ~> (b ~> a) ~> a
, prove $ (((a ~> a ~> a) ~> b ~> a ~> a) ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> (b ~> a) ~> a ~> c) ~> a ~> c
, prove $ (a ~> a ~> a) ~> ((b ~> a ~> a) ~> c) ~> a ~> c
, prove $ (a ~> a ~> a) ~> b ~> ((a ~> a) ~> c) ~> a ~> c
, prove $ (a ~> a) ~> (a ~> (b ~> a ~> a) ~> c) ~> a ~> c
, prove $ a ~> (a ~> a ~> b) ~> (a ~> a) ~> c ~> b
, prove $ a ~> (a ~> a ~> b ~> a ~> a ~> c) ~> b ~> c
, prove $ (a ~> a) ~> a ~> ((b ~> a) ~> a ~> c) ~> c
, prove $ (a ~> a) ~> a ~> b ~> (a ~> a ~> c) ~> c
, prove $ a ~> (((a ~> a) ~> b ~> a) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> (b ~> a) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a) ~> ((b ~> a) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a) ~> b ~> (a ~> a ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> a) ~> c ~> d ~> a
, prove $ a ~> (a ~> a ~> (b ~> a) ~> a ~> c) ~> d ~> c
, prove $ (((a ~> a) ~> a) ~> b) ~> a ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> a ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> a ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> b
, prove $ (a ~> a ~> a) ~> b ~> a ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> a ~> b
, prove $ a ~> (a ~> a ~> b) ~> a ~> b
, prove $ (a ~> a ~> a) ~> (b ~> a) ~> b ~> a ~> a
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> b) ~> a) ~> a ~> a ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> (b ~> a) ~> a ~> a ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> ((a ~> b) ~> (a ~> a) ~> a) ~> b
, prove $ (a ~> a ~> a ~> b ~> a) ~> b ~> a ~> a ~> a ~> b ~> a
, prove $ (((a ~> a ~> a ~> b) ~> a ~> b) ~> (a ~> a ~> a ~> b) ~> a ~> b) ~> (a ~> a ~> a ~> b) ~> a ~> b
, prove $ a ~> ((a ~> a ~> b) ~> (a ~> b) ~> a) ~> (a ~> a ~> b) ~> b
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> b) ~> (a ~> a ~> a ~> b) ~> b) ~> (a ~> a ~> a ~> b) ~> b
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> b) ~> (a ~> a ~> a ~> b) ~> c) ~> c
, prove $ (a ~> a ~> a ~> b) ~> a ~> (b ~> (a ~> a ~> a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> b) ~> a ~> a) ~> b
, prove $ a ~> (a ~> a ~> b) ~> (a ~> b ~> a) ~> a ~> b
, prove $ a ~> ((a ~> a ~> b ~> a) ~> b) ~> (a ~> a ~> b ~> a) ~> a ~> b ~> a
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> b) ~> (a ~> a ~> b) ~> a) ~> b
, prove $ (a ~> a) ~> ((a ~> b) ~> (a ~> b) ~> a) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> (a ~> b ~> (a ~> a ~> b) ~> c) ~> c
, prove $ (a ~> a) ~> (a ~> b) ~> ((a ~> b) ~> a) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> b) ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> b ~> a) ~> b ~> a ~> b ~> a
, prove $ (a ~> a) ~> a ~> ((b ~> a) ~> b ~> a) ~> b ~> a
, prove $ a ~> (a ~> a ~> b ~> a) ~> b ~> a ~> b ~> a
, prove $ a ~> (a ~> a ~> b) ~> (a ~> b ~> a) ~> b ~> a
, prove $ a ~> (a ~> a) ~> ((b ~> a) ~> b ~> a) ~> b ~> a
, prove $ a ~> a ~> (a ~> (b ~> a) ~> b ~> a) ~> b ~> a
, prove $ (a ~> a ~> ((a ~> b) ~> a) ~> b) ~> ((a ~> b) ~> a) ~> a ~> ((a ~> b) ~> a) ~> b
, prove $ a ~> (a ~> (a ~> b ~> a) ~> b) ~> (a ~> b ~> a) ~> (a ~> b ~> a) ~> b
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> b) ~> a ~> b) ~> a ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> ((a ~> b) ~> (a ~> b) ~> a) ~> b
, prove $ a ~> (a ~> (a ~> b ~> a) ~> b) ~> (a ~> b ~> a) ~> b ~> a
, prove $ a ~> (a ~> ((a ~> b) ~> a ~> b) ~> a ~> b) ~> ((a ~> b) ~> a ~> b) ~> b
, prove $ a ~> (((a ~> a ~> b) ~> a ~> b) ~> a ~> b) ~> b
, prove $ a ~> (a ~> (a ~> b) ~> a ~> b) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> b) ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> b) ~> a ~> b) ~> c ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> ((a ~> b) ~> a) ~> c ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> b) ~> a) ~> c ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> (b ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (a ~> b ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> b ~> a) ~> b ~> b ~> a
, prove $ a ~> (a ~> a ~> (b ~> a) ~> b) ~> (b ~> a) ~> a ~> (b ~> a) ~> b
, prove $ (a ~> a ~> ((a ~> b) ~> a ~> b) ~> b) ~> ((a ~> b) ~> a ~> b) ~> a ~> b
, prove $ (((a ~> a ~> a ~> b) ~> a ~> b) ~> b) ~> b
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> b) ~> b) ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> (b ~> b) ~> b
, prove $ a ~> (a ~> (a ~> b) ~> (a ~> b) ~> b ~> c) ~> (a ~> b) ~> c
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> b) ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((a ~> b) ~> b ~> c) ~> c
, prove $ ((a ~> a ~> a ~> b) ~> (a ~> b) ~> c) ~> (a ~> a ~> a ~> b) ~> c
, prove $ a ~> ((a ~> a ~> b) ~> a ~> b ~> c) ~> (a ~> a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b ~> a) ~> b ~> c ~> a ~> b ~> a
, prove $ a ~> (a ~> (a ~> b) ~> a ~> b ~> c) ~> (a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b ~> (a ~> b) ~> c) ~> (a ~> b) ~> c
, prove $ (a ~> a ~> a ~> b) ~> (a ~> b ~> c) ~> a ~> c
, prove $ a ~> (a ~> a ~> b ~> a ~> b ~> c) ~> b ~> c
, prove $ (((((a ~> a) ~> a) ~> b) ~> a ~> b) ~> c) ~> c
, prove $ (((a ~> a ~> a ~> b) ~> a ~> b) ~> c) ~> c
, prove $ (((a ~> a) ~> (a ~> b) ~> a ~> b) ~> c) ~> c
, prove $ (((a ~> a) ~> a) ~> b) ~> ((a ~> b) ~> c) ~> c
, prove $ (((a ~> a) ~> a) ~> b) ~> a ~> (b ~> c) ~> c
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> b) ~> c) ~> c
, prove $ (a ~> a ~> a ~> b) ~> a ~> (b ~> c) ~> c
, prove $ (a ~> a) ~> (((a ~> b) ~> a ~> b) ~> c) ~> c
, prove $ (a ~> a) ~> (a ~> b) ~> ((a ~> b) ~> c) ~> c
, prove $ (a ~> a) ~> (a ~> b) ~> a ~> (b ~> c) ~> c
, prove $ (a ~> a) ~> a ~> b ~> (a ~> b ~> c) ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (a ~> b ~> c) ~> c
, prove $ a ~> (a ~> a) ~> b ~> (a ~> b ~> c) ~> c
, prove $ (((a ~> a ~> a ~> b) ~> a ~> b) ~> c) ~> d ~> c
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> b) ~> c) ~> d ~> c
, prove $ (a ~> a ~> a ~> b) ~> a ~> (b ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> b) ~> (a ~> b ~> c) ~> d ~> c
, prove $ (a ~> a ~> a ~> b) ~> a ~> c ~> a
, prove $ (a ~> a ~> a) ~> b ~> a ~> c ~> a
, prove $ a ~> (a ~> a ~> (b ~> a) ~> c) ~> a
, prove $ (a ~> a ~> a) ~> b ~> a ~> c ~> a ~> a
, prove $ (a ~> a ~> a ~> b) ~> a ~> c ~> a ~> a ~> a ~> b
, prove $ ((((a ~> a) ~> a) ~> b) ~> a) ~> c ~> (((a ~> a) ~> a) ~> b) ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> a ~> c ~> (a ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> a ~> c ~> (a ~> a) ~> b
, prove $ a ~> (a ~> a ~> (b ~> a) ~> c) ~> a ~> a ~> (b ~> a) ~> c
, prove $ a ~> (a ~> a ~> b ~> a ~> c) ~> ((a ~> a ~> b ~> a ~> c) ~> b) ~> c
, prove $ ((((a ~> a) ~> a) ~> b ~> a) ~> c) ~> (a ~> a) ~> c
, prove $ ((a ~> a) ~> (a ~> b ~> a) ~> c) ~> (a ~> a) ~> c
, prove $ ((a ~> a) ~> a) ~> ((b ~> a) ~> c) ~> (a ~> a) ~> c
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> c) ~> (a ~> a) ~> c
, prove $ a ~> ((a ~> a) ~> (b ~> a) ~> c) ~> (a ~> a) ~> c
, prove $ (a ~> a) ~> ((a ~> b) ~> a) ~> c ~> (a ~> b) ~> b
, prove $ (a ~> a ~> a ~> b ~> a ~> c) ~> a ~> b ~> c
, prove $ a ~> (a ~> a ~> b ~> a ~> c) ~> (a ~> b) ~> c
, prove $ (((a ~> a) ~> a) ~> (b ~> a) ~> c) ~> a ~> c
, prove $ (a ~> ((a ~> a) ~> b ~> a) ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> (b ~> a) ~> c) ~> a ~> c
, prove $ (a ~> a) ~> (a ~> (b ~> a) ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> (b ~> a) ~> c) ~> a ~> d ~> c
, prove $ a ~> (a ~> a ~> (b ~> a) ~> (c ~> a) ~> d) ~> d
, prove $ (((a ~> a) ~> a) ~> b) ~> a ~> c ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> c ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> a ~> c ~> b
, prove $ a ~> (a ~> a ~> b) ~> (a ~> c) ~> b
, prove $ a ~> ((a ~> a ~> b ~> a ~> c) ~> b) ~> (a ~> a ~> b ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> b ~> a) ~> c ~> b ~> a ~> b ~> a
, prove $ a ~> (a ~> (a ~> b ~> a ~> c) ~> b) ~> (a ~> b ~> a ~> c) ~> c
, prove $ (a ~> a ~> a ~> b ~> a ~> c) ~> b ~> a ~> c
, prove $ a ~> (a ~> a ~> (b ~> a ~> c) ~> b) ~> (b ~> a ~> c) ~> c
, prove $ (a ~> a) ~> a ~> (b ~> a ~> c) ~> b ~> c
, prove $ a ~> (a ~> a ~> b ~> a ~> c) ~> b ~> c
, prove $ a ~> (a ~> a) ~> (b ~> a ~> c) ~> b ~> c
, prove $ a ~> (a ~> a ~> b ~> a ~> c) ~> b ~> d ~> c
, prove $ (((a ~> a ~> a ~> b) ~> a ~> c ~> b) ~> d) ~> d
, prove $ (a ~> a ~> a ~> b) ~> ((a ~> c ~> b) ~> d) ~> d
, prove $ (a ~> a ~> a ~> b) ~> a ~> ((c ~> b) ~> d) ~> d
, prove $ (a ~> a ~> a ~> b) ~> a ~> c ~> (b ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> (a ~> (c ~> b) ~> d) ~> d
, prove $ ((((a ~> a) ~> a) ~> b ~> a) ~> c) ~> c
, prove $ (((a ~> a) ~> a ~> b ~> a) ~> c) ~> c
, prove $ ((a ~> (a ~> a ~> b) ~> a) ~> c) ~> c
, prove $ ((a ~> (a ~> a) ~> b ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> ((b ~> a) ~> c) ~> c
, prove $ ((a ~> a) ~> a) ~> b ~> (a ~> c) ~> c
, prove $ (a ~> a ~> a ~> b) ~> a ~> c ~> c
, prove $ (a ~> a) ~> ((a ~> b ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> a ~> ((b ~> a) ~> c) ~> c
, prove $ (a ~> a) ~> a ~> b ~> (a ~> c) ~> c
, prove $ a ~> (((a ~> a ~> b) ~> a) ~> c) ~> c
, prove $ a ~> (((a ~> a) ~> b ~> a) ~> c) ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a ~> (b ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (a ~> c) ~> c
, prove $ a ~> (a ~> a) ~> ((b ~> a) ~> c) ~> c
, prove $ a ~> (a ~> a) ~> b ~> (a ~> c) ~> c
, prove $ ((a ~> (a ~> a ~> (b ~> a) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (((a ~> a ~> (b ~> a) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> (b ~> a) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (((b ~> a) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> (a ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> a) ~> (c ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> a) ~> c) ~> (c ~> d) ~> d
, prove $ (a ~> a ~> a) ~> b ~> a ~> c ~> d ~> a ~> a
, prove $ (a ~> a ~> a ~> (b ~> a) ~> c) ~> d ~> a ~> c
, prove $ (((a ~> a) ~> a) ~> b) ~> a ~> c ~> d ~> b
, prove $ (a ~> a ~> a ~> b) ~> a ~> c ~> d ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> a ~> c ~> d ~> b
, prove $ a ~> (a ~> a ~> b ~> a ~> c) ~> d ~> b ~> c
, prove $ (((a ~> a) ~> a ~> b ~> a) ~> c) ~> d ~> c
, prove $ ((a ~> (a ~> a) ~> b ~> a) ~> c) ~> d ~> c
, prove $ (a ~> a) ~> ((a ~> b ~> a) ~> c) ~> d ~> c
, prove $ (a ~> a) ~> a ~> ((b ~> a) ~> c) ~> d ~> c
, prove $ (a ~> a) ~> a ~> b ~> (a ~> c) ~> d ~> c
, prove $ a ~> (((a ~> a) ~> b ~> a) ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> (b ~> a) ~> c) ~> d ~> c
, prove $ a ~> (a ~> a) ~> ((b ~> a) ~> c) ~> d ~> c
, prove $ a ~> (a ~> a) ~> b ~> (a ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> (b ~> a) ~> c ~> d) ~> c ~> d
, prove $ (a ~> a ~> a ~> b) ~> a ~> c ~> d ~> e ~> b
, prove $ a ~> (a ~> a ~> (b ~> a) ~> c) ~> d ~> e ~> c
, prove $ ((a ~> a) ~> a) ~> b ~> b
, prove $ (a ~> a ~> a) ~> b ~> b
, prove $ (a ~> a) ~> a ~> b ~> b
, prove $ a ~> ((a ~> a) ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a) ~> b ~> b
, prove $ a ~> a ~> (a ~> b) ~> b
, prove $ (a ~> a ~> a) ~> b ~> (b ~> a) ~> a ~> a
, prove $ (a ~> a ~> a ~> b) ~> (b ~> a) ~> a ~> a ~> a ~> b
, prove $ (a ~> ((a ~> a ~> b) ~> b) ~> a) ~> a ~> ((a ~> a ~> b) ~> b) ~> a
, prove $ (a ~> a ~> ((a ~> b) ~> b) ~> a) ~> a ~> a ~> ((a ~> b) ~> b) ~> a
, prove $ (a ~> a ~> a ~> (b ~> b) ~> a) ~> a ~> a ~> a ~> (b ~> b) ~> a
, prove $ a ~> (a ~> a ~> b) ~> (b ~> a ~> a) ~> a ~> b
, prove $ a ~> ((a ~> a ~> b) ~> b ~> a) ~> (a ~> a ~> b) ~> a ~> b
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> a ~> a) ~> ((a ~> b) ~> b) ~> a ~> a
, prove $ a ~> (a ~> a ~> (b ~> b) ~> a ~> a) ~> a ~> (b ~> b) ~> a ~> a
, prove $ (((a ~> a ~> a ~> b) ~> b) ~> (a ~> a ~> a ~> b) ~> b) ~> a ~> (a ~> a ~> a ~> b) ~> b
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> a ~> (a ~> a ~> b) ~> b) ~> a ~> (a ~> a ~> b) ~> b
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> a ~> (a ~> a ~> b) ~> b) ~> a ~> (a ~> a ~> b) ~> b
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> a ~> (a ~> a ~> b) ~> b) ~> c ~> a ~> (a ~> a ~> b) ~> b
, prove $ (a ~> a ~> a ~> b) ~> (b ~> (a ~> a ~> a ~> b) ~> c) ~> a ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> a ~> (a ~> a ~> b) ~> c) ~> c
, prove $ ((a ~> a) ~> a ~> b) ~> (b ~> a) ~> a ~> b
, prove $ a ~> (a ~> a ~> b) ~> (b ~> a) ~> a ~> b
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (a ~> a ~> b) ~> a) ~> a ~> b
, prove $ a ~> ((a ~> a ~> b) ~> b ~> a ~> a ~> b) ~> (a ~> a ~> b) ~> b ~> a ~> a ~> b
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (a ~> a ~> b) ~> (a ~> a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> (a ~> b) ~> b ~> a) ~> (a ~> b) ~> (a ~> b) ~> b ~> a
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (a ~> a ~> b) ~> a ~> c) ~> c
, prove $ a ~> (a ~> (a ~> b) ~> b ~> a) ~> (a ~> b) ~> b
, prove $ ((a ~> a) ~> ((a ~> b) ~> b) ~> a) ~> ((a ~> b) ~> b) ~> a
, prove $ ((a ~> a) ~> a ~> (b ~> b) ~> a) ~> a ~> (b ~> b) ~> a
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> a) ~> ((a ~> b) ~> b) ~> a
, prove $ a ~> (a ~> a ~> (b ~> b) ~> a) ~> a ~> (b ~> b) ~> a
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> (a ~> a ~> b) ~> b) ~> (a ~> a ~> b) ~> b
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> (a ~> a ~> b) ~> b) ~> (a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (a ~> a ~> b) ~> b) ~> (a ~> a ~> b) ~> b
, prove $ a ~> ((a ~> (a ~> b) ~> b) ~> a ~> (a ~> b) ~> b) ~> (a ~> b) ~> b
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> (a ~> a ~> b) ~> b) ~> c ~> (a ~> a ~> b) ~> b
, prove $ a ~> ((a ~> a ~> b) ~> b ~> (a ~> a ~> b) ~> c) ~> (a ~> a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (a ~> a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (a ~> a ~> b) ~> c) ~> d ~> c
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> a ~> a ~> c) ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> a ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> (b ~> b) ~> a ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> a ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> a) ~> b
, prove $ a ~> (a ~> a ~> b) ~> (b ~> a ~> b) ~> a ~> b
, prove $ a ~> (a ~> a ~> b ~> b ~> a) ~> b ~> a ~> b ~> b ~> a
, prove $ (a ~> a ~> ((a ~> b) ~> b) ~> a ~> b) ~> ((a ~> b) ~> b) ~> b
, prove $ a ~> (a ~> (a ~> b) ~> b) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> a ~> (b ~> b) ~> a) ~> (b ~> b) ~> a
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> (a ~> b) ~> b) ~> (a ~> b) ~> b
, prove $ a ~> (a ~> (a ~> b) ~> b ~> (a ~> b) ~> c) ~> (a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (a ~> b) ~> c) ~> c
, prove $ a ~> ((a ~> a ~> b) ~> b ~> a ~> c) ~> (a ~> a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> a) ~> c ~> a ~> b
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> a) ~> c ~> ((a ~> b) ~> b) ~> a
, prove $ a ~> (a ~> a ~> (b ~> b) ~> a) ~> c ~> a ~> (b ~> b) ~> a
, prove $ a ~> (a ~> (a ~> b) ~> b ~> a ~> c) ~> (a ~> b) ~> c
, prove $ (((a ~> a ~> a ~> b) ~> b) ~> a ~> c) ~> a ~> c
, prove $ (a ~> ((a ~> a ~> b) ~> b) ~> a ~> c) ~> a ~> c
, prove $ (a ~> a ~> ((a ~> b) ~> b) ~> a ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> (b ~> b) ~> a ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> b) ~> (b ~> a ~> c) ~> a ~> c
, prove $ a ~> (a ~> a ~> b ~> b ~> a ~> c) ~> b ~> c
, prove $ (a ~> a) ~> a ~> ((b ~> b) ~> a ~> c) ~> c
, prove $ (a ~> a) ~> a ~> b ~> (b ~> a ~> c) ~> c
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> a ~> c) ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> (b ~> b) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> a ~> c) ~> c
, prove $ a ~> (a ~> a) ~> ((b ~> b) ~> a ~> c) ~> c
, prove $ a ~> (a ~> a) ~> b ~> (b ~> a ~> c) ~> c
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> a ~> c) ~> d ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> a ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> (b ~> b) ~> a ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> a ~> c) ~> d ~> c
, prove $ (a ~> a ~> a ~> b) ~> (b ~> b) ~> a ~> b
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> (b ~> b) ~> b
, prove $ a ~> a ~> (a ~> b ~> b) ~> b ~> b
, prove $ a ~> (a ~> a ~> (b ~> b) ~> b) ~> (b ~> b) ~> b
, prove $ a ~> a ~> (a ~> (b ~> b) ~> b ~> b) ~> b ~> b
, prove $ a ~> (a ~> a ~> b) ~> (b ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> b ~> b ~> b ~> c) ~> b ~> c
, prove $ a ~> a ~> (a ~> b) ~> (b ~> b ~> c) ~> c
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> c) ~> a
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> c) ~> a
, prove $ a ~> (a ~> a ~> (b ~> b) ~> c) ~> a
, prove $ a ~> (a ~> a ~> b) ~> (b ~> c) ~> a
, prove $ ((a ~> a ~> a ~> b) ~> b ~> c) ~> a ~> (a ~> a ~> a ~> b) ~> c
, prove $ ((a ~> a ~> a ~> b) ~> b ~> c) ~> (a ~> a ~> a ~> b) ~> a ~> c
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> c) ~> (a ~> (a ~> a ~> b) ~> b) ~> c
, prove $ (a ~> (a ~> a ~> b) ~> b ~> c) ~> a ~> (a ~> a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> c) ~> a ~> a ~> b
, prove $ (a ~> (a ~> a ~> b) ~> b ~> c) ~> (a ~> a ~> b) ~> a ~> c
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> c) ~> ((a ~> a ~> b) ~> b) ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> c) ~> a ~> ((a ~> b) ~> b) ~> c
, prove $ a ~> (a ~> a ~> (b ~> b) ~> c) ~> a ~> a ~> (b ~> b) ~> c
, prove $ (a ~> a ~> (a ~> b) ~> b ~> c) ~> a ~> (a ~> b) ~> c
, prove $ a ~> ((a ~> a ~> b) ~> b ~> c) ~> (a ~> a ~> b) ~> c
, prove $ a ~> ((a ~> a ~> b) ~> b ~> c) ~> (a ~> a ~> b) ~> d ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (c ~> a ~> a ~> b) ~> d) ~> d
, prove $ (a ~> a ~> (a ~> b) ~> b ~> c) ~> (a ~> b) ~> a ~> c
, prove $ (a ~> a ~> a ~> b ~> b ~> c) ~> a ~> b ~> c
, prove $ a ~> (a ~> (a ~> b) ~> b ~> c) ~> (a ~> b) ~> c
, prove $ a ~> (a ~> (a ~> b) ~> b ~> c) ~> (a ~> b) ~> d ~> c
, prove $ (((((a ~> a) ~> a) ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (((a ~> a ~> a ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (((a ~> a) ~> (a ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (((a ~> a) ~> a) ~> (b ~> b) ~> c) ~> a ~> c
, prove $ (((a ~> a) ~> a) ~> b) ~> (b ~> c) ~> a ~> c
, prove $ (a ~> ((a ~> a ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (a ~> a ~> ((a ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> (b ~> b) ~> c) ~> a ~> c
, prove $ (a ~> a ~> a ~> b) ~> (b ~> c) ~> a ~> c
, prove $ (a ~> a) ~> (((a ~> b) ~> b) ~> c) ~> a ~> c
, prove $ (a ~> a) ~> (a ~> (b ~> b) ~> c) ~> a ~> c
, prove $ (a ~> a) ~> (a ~> b) ~> (b ~> c) ~> a ~> c
, prove $ (((a ~> a ~> a ~> b) ~> b) ~> c) ~> a ~> d ~> c
, prove $ (a ~> ((a ~> a ~> b) ~> b) ~> c) ~> a ~> d ~> c
, prove $ (a ~> a ~> ((a ~> b) ~> b) ~> c) ~> a ~> d ~> c
, prove $ (a ~> a ~> a ~> (b ~> b) ~> c) ~> a ~> d ~> c
, prove $ (a ~> a ~> a ~> b) ~> (b ~> c) ~> a ~> d ~> c
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> (c ~> a) ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> (c ~> a) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> b) ~> (c ~> a) ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (c ~> a) ~> d) ~> d
, prove $ (a ~> a ~> a ~> b ~> b ~> c) ~> b ~> a ~> c
, prove $ a ~> (a ~> a ~> b ~> b ~> c) ~> b ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> c) ~> b ~> c
, prove $ a ~> (a ~> a ~> b ~> b ~> c) ~> b ~> d ~> c
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> (b ~> b) ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> c) ~> c
, prove $ ((((a ~> (a ~> a ~> b) ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ ((a ~> (((a ~> a ~> b) ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ ((a ~> (a ~> ((a ~> b) ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ ((a ~> (a ~> a ~> (b ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ ((a ~> (a ~> a ~> b) ~> (b ~> c) ~> c) ~> d) ~> d
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> (c ~> c) ~> d) ~> d
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> c) ~> (c ~> d) ~> d
, prove $ a ~> (((((a ~> a ~> b) ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (((a ~> ((a ~> b) ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (((a ~> a ~> (b ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (((a ~> a ~> b) ~> (b ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> (c ~> c) ~> d) ~> d
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> c) ~> (c ~> d) ~> d
, prove $ a ~> (a ~> ((((a ~> b) ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> (b ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> b) ~> (b ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> (c ~> c) ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> c) ~> (c ~> d) ~> d
, prove $ a ~> (a ~> a ~> (((b ~> b) ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> (b ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> b) ~> (c ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> b) ~> c) ~> (c ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> (((b ~> c) ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> (b ~> (c ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> (b ~> c) ~> (c ~> d) ~> d
, prove $ a ~> ((a ~> a ~> b) ~> b ~> c) ~> d ~> (a ~> a ~> b) ~> c
, prove $ a ~> (a ~> (a ~> b) ~> b ~> c) ~> d ~> (a ~> b) ~> c
, prove $ (((a ~> a ~> a ~> b) ~> b) ~> c) ~> d ~> a ~> c
, prove $ (a ~> ((a ~> a ~> b) ~> b) ~> c) ~> d ~> a ~> c
, prove $ (a ~> a ~> ((a ~> b) ~> b) ~> c) ~> d ~> a ~> c
, prove $ (a ~> a ~> a ~> (b ~> b) ~> c) ~> d ~> a ~> c
, prove $ (a ~> a ~> a ~> b) ~> (b ~> c) ~> d ~> a ~> c
, prove $ a ~> (a ~> a ~> b ~> b ~> c) ~> d ~> b ~> c
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> c) ~> d ~> c
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> c) ~> d ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> (b ~> b) ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> c) ~> d ~> c
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> c ~> d) ~> c ~> d
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> c ~> d) ~> c ~> d
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> c ~> d) ~> c ~> d
, prove $ a ~> (a ~> a ~> (b ~> b) ~> c ~> d) ~> c ~> d
, prove $ a ~> (a ~> a ~> b) ~> (b ~> c ~> d) ~> c ~> d
, prove $ ((a ~> (a ~> a ~> b) ~> b) ~> c) ~> d ~> e ~> c
, prove $ a ~> (((a ~> a ~> b) ~> b) ~> c) ~> d ~> e ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> b) ~> c) ~> d ~> e ~> c
, prove $ a ~> (a ~> a ~> (b ~> b) ~> c) ~> d ~> e ~> c
, prove $ a ~> (a ~> a ~> b) ~> (b ~> c) ~> d ~> e ~> c
, prove $ ((a ~> a) ~> a) ~> b ~> c ~> a
, prove $ (a ~> a) ~> a ~> b ~> c ~> a
, prove $ a ~> (a ~> a ~> b ~> c) ~> a
, prove $ a ~> (a ~> a ~> b) ~> c ~> a
, prove $ a ~> (a ~> a) ~> b ~> c ~> a
, prove $ (a ~> a ~> a ~> b) ~> c ~> a ~> a
, prove $ (a ~> a ~> a) ~> b ~> c ~> a ~> a
, prove $ (a ~> a) ~> a ~> b ~> c ~> a ~> a
, prove $ a ~> (a ~> a) ~> b ~> c ~> a ~> a
, prove $ ((a ~> a) ~> a) ~> b ~> c ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a) ~> b ~> c ~> a ~> a ~> a
, prove $ (a ~> a ~> a ~> b) ~> c ~> a ~> a ~> a ~> a ~> b
, prove $ (a ~> a ~> a ~> b ~> c) ~> a ~> ((a ~> a ~> a ~> b ~> c) ~> b) ~> c
, prove $ (((a ~> a) ~> a) ~> b) ~> ((c ~> a ~> a) ~> a) ~> b
, prove $ (((a ~> a) ~> a) ~> b) ~> c ~> ((a ~> a) ~> a) ~> b
, prove $ ((a ~> a ~> a) ~> b) ~> c ~> (a ~> a ~> a) ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> c ~> (a ~> a) ~> a ~> b
, prove $ ((a ~> a) ~> a ~> b) ~> c ~> a ~> (a ~> a) ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> c ~> (a ~> a) ~> a ~> b
, prove $ (a ~> (a ~> a) ~> b) ~> c ~> a ~> (a ~> a) ~> b
, prove $ (a ~> a ~> a ~> b) ~> c ~> a ~> a ~> a ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> ((c ~> a ~> a) ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> c ~> ((a ~> a) ~> a) ~> b
, prove $ a ~> ((a ~> a) ~> b) ~> c ~> (a ~> a ~> a) ~> b
, prove $ (((a ~> a) ~> a) ~> b) ~> ((c ~> ((a ~> a) ~> a) ~> b) ~> a) ~> b
, prove $ (((a ~> a) ~> a) ~> b) ~> c ~> ((((a ~> a) ~> a) ~> b) ~> a) ~> b
, prove $ a ~> (a ~> a ~> (b ~> c ~> a) ~> a) ~> a ~> (b ~> c ~> a) ~> a
, prove $ (a ~> a ~> a ~> b ~> c) ~> ((a ~> a ~> a ~> b ~> c) ~> b) ~> a ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> (a ~> (a ~> a ~> b ~> c) ~> b) ~> c
, prove $ a ~> (a ~> a ~> b) ~> c ~> (a ~> a) ~> b
, prove $ a ~> (a ~> a ~> b) ~> c ~> a ~> a ~> b
, prove $ a ~> (a ~> a ~> b) ~> c ~> ((a ~> a ~> b) ~> a ~> a ~> b) ~> b
, prove $ (a ~> ((a ~> a) ~> b) ~> c) ~> ((a ~> a) ~> b) ~> b
, prove $ a ~> ((a ~> a ~> b) ~> c) ~> (a ~> a ~> b) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> a ~> a ~> b) ~> b ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> c ~> ((a ~> a ~> b) ~> b ~> d) ~> d
, prove $ ((a ~> a ~> a ~> b) ~> c) ~> (a ~> a ~> b) ~> c
, prove $ (a ~> a ~> a ~> b ~> c) ~> a ~> (a ~> b) ~> c
, prove $ a ~> ((a ~> a ~> b) ~> c) ~> (a ~> a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> (a ~> a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> a ~> a ~> b ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> ((a ~> a ~> b ~> c) ~> (a ~> a ~> b ~> c) ~> b) ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> ((a ~> a ~> b ~> c) ~> a ~> b) ~> c
, prove $ a ~> ((a ~> a ~> b ~> c) ~> (a ~> a ~> b ~> c) ~> b) ~> (a ~> a ~> b ~> c) ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> ((a ~> a ~> b ~> c) ~> b) ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> ((a ~> a ~> b ~> c) ~> b) ~> d ~> c
, prove $ ((a ~> a) ~> a) ~> b ~> c ~> (a ~> a) ~> d ~> a
, prove $ a ~> (a ~> a ~> (b ~> c ~> a) ~> a ~> d) ~> d
, prove $ (((a ~> a) ~> a) ~> b) ~> c ~> a ~> b
, prove $ (a ~> a ~> a ~> b) ~> c ~> a ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> c ~> a ~> b
, prove $ a ~> (a ~> a ~> b) ~> c ~> a ~> b
, prove $ a ~> ((a ~> a ~> b ~> c) ~> a ~> b) ~> (a ~> a ~> b ~> c) ~> c
, prove $ (a ~> a) ~> (a ~> b) ~> ((c ~> a ~> b) ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> c ~> ((a ~> b) ~> a) ~> b
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> a ~> b) ~> a) ~> b
, prove $ a ~> (a ~> a ~> b) ~> c ~> ((a ~> b) ~> a) ~> b
, prove $ a ~> (a ~> a ~> b) ~> c ~> ((a ~> b) ~> a ~> b) ~> b
, prove $ (a ~> a ~> ((a ~> b) ~> c) ~> a ~> b) ~> ((a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> (a ~> b ~> c) ~> a ~> b) ~> (a ~> b ~> c) ~> c
, prove $ (a ~> a ~> a ~> b ~> c) ~> (a ~> b) ~> a ~> c
, prove $ a ~> (a ~> (a ~> b) ~> c) ~> (a ~> b) ~> b
, prove $ (a ~> a ~> a ~> b) ~> c ~> ((a ~> b) ~> b) ~> b
, prove $ a ~> (a ~> a ~> (b ~> c) ~> a ~> b) ~> (b ~> c) ~> c
, prove $ (((a ~> a) ~> a ~> b) ~> c) ~> (a ~> b) ~> c
, prove $ (((a ~> a) ~> a) ~> b ~> c) ~> a ~> b ~> c
, prove $ ((a ~> (a ~> a) ~> b) ~> c) ~> (a ~> b) ~> c
, prove $ ((a ~> a) ~> (a ~> b) ~> c) ~> (a ~> b) ~> c
, prove $ (a ~> a ~> a ~> b ~> c) ~> a ~> b ~> c
, prove $ (a ~> a) ~> ((a ~> b) ~> c) ~> (a ~> b) ~> c
, prove $ (a ~> a) ~> (a ~> b ~> c) ~> a ~> b ~> c
, prove $ (a ~> a) ~> a ~> (b ~> c) ~> (a ~> b) ~> c
, prove $ a ~> (((a ~> a) ~> b) ~> c) ~> (a ~> b) ~> c
, prove $ a ~> (a ~> (a ~> b) ~> c) ~> (a ~> b) ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> (a ~> b) ~> c
, prove $ a ~> (a ~> a) ~> (b ~> c) ~> (a ~> b) ~> c
, prove $ (a ~> a ~> ((a ~> b) ~> c) ~> ((a ~> b) ~> c) ~> b) ~> ((a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> (a ~> b ~> c) ~> (a ~> b ~> c) ~> b) ~> (a ~> b ~> c) ~> c
, prove $ a ~> (a ~> (a ~> b) ~> c) ~> (((a ~> b) ~> c) ~> b) ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> ((a ~> b ~> c) ~> b) ~> c
, prove $ (a ~> a ~> a ~> b ~> c) ~> ((a ~> b ~> c) ~> c) ~> c
, prove $ (a ~> a ~> a ~> b ~> c) ~> a ~> b ~> d ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> (a ~> b) ~> d ~> c
, prove $ (((a ~> a ~> a ~> b) ~> c ~> a ~> b) ~> d) ~> d
, prove $ (a ~> a ~> a ~> b) ~> ((c ~> a ~> b) ~> d) ~> d
, prove $ (a ~> a ~> a ~> b) ~> c ~> ((a ~> b) ~> d) ~> d
, prove $ (a ~> a ~> a ~> b) ~> c ~> a ~> (b ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> a) ~> b ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> c ~> (a ~> b ~> d) ~> d
, prove $ (a ~> a ~> a ~> b) ~> c ~> a ~> c
, prove $ a ~> (a ~> a ~> (b ~> c) ~> a) ~> c ~> a ~> (b ~> c) ~> a
, prove $ (((a ~> a) ~> a) ~> b) ~> (c ~> a) ~> c ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> (c ~> a) ~> c ~> b
, prove $ (a ~> a ~> a) ~> b ~> c ~> a ~> d ~> a ~> a
, prove $ (a ~> a ~> a ~> (b ~> c ~> a) ~> d) ~> a ~> d
, prove $ (((a ~> a) ~> a) ~> b) ~> c ~> a ~> d ~> b
, prove $ (a ~> a ~> a ~> b) ~> c ~> a ~> d ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> c ~> a ~> d ~> b
, prove $ (a ~> a ~> a ~> b ~> c) ~> a ~> d ~> b ~> c
, prove $ a ~> (a ~> a ~> b ~> (c ~> a) ~> d) ~> b ~> d
, prove $ a ~> (a ~> a ~> (b ~> c) ~> a ~> d) ~> c ~> d
, prove $ (((a ~> a) ~> a ~> b ~> c ~> a) ~> d) ~> d
, prove $ ((a ~> (a ~> a) ~> b ~> c ~> a) ~> d) ~> d
, prove $ (a ~> a) ~> ((a ~> b ~> c ~> a) ~> d) ~> d
, prove $ (a ~> a) ~> a ~> ((b ~> c ~> a) ~> d) ~> d
, prove $ (a ~> a) ~> a ~> b ~> ((c ~> a) ~> d) ~> d
, prove $ (a ~> a) ~> a ~> b ~> c ~> (a ~> d) ~> d
, prove $ a ~> (((a ~> a) ~> b ~> c ~> a) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> c ~> a) ~> d) ~> d
, prove $ a ~> (a ~> a) ~> ((b ~> c ~> a) ~> d) ~> d
, prove $ a ~> (a ~> a) ~> b ~> ((c ~> a) ~> d) ~> d
, prove $ a ~> (a ~> a) ~> b ~> c ~> (a ~> d) ~> d
, prove $ (a ~> a ~> a ~> b) ~> c ~> a ~> d ~> e ~> b
, prove $ a ~> (a ~> a ~> (b ~> c ~> a) ~> d) ~> e ~> d
, prove $ (a ~> a) ~> a ~> b ~> c ~> b
, prove $ a ~> (a ~> a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a) ~> b ~> c ~> b
, prove $ a ~> a ~> (a ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> b ~> c) ~> b ~> a
, prove $ ((a ~> a ~> a ~> b ~> c) ~> b) ~> a ~> (a ~> a ~> a ~> b ~> c) ~> c
, prove $ ((a ~> a ~> a ~> b ~> c) ~> b) ~> (a ~> a ~> a ~> b ~> c) ~> a ~> c
, prove $ ((a ~> (a ~> a ~> b) ~> c ~> b) ~> a ~> (a ~> a ~> b) ~> c ~> b) ~> a ~> (a ~> a ~> b) ~> c ~> b
, prove $ (a ~> (a ~> a ~> b ~> c) ~> b) ~> a ~> (a ~> a ~> b ~> c) ~> c
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> b) ~> a) ~> a ~> b
, prove $ a ~> (a ~> a ~> b) ~> c ~> (b ~> a) ~> a ~> b
, prove $ a ~> (a ~> a ~> b ~> c) ~> b ~> a ~> a ~> b ~> c
, prove $ (a ~> (a ~> a ~> b ~> c) ~> b) ~> (a ~> a ~> b ~> c) ~> a ~> c
, prove $ a ~> (a ~> ((a ~> b) ~> c ~> b) ~> a) ~> ((a ~> b) ~> c ~> b) ~> a
, prove $ a ~> (a ~> a ~> (b ~> c ~> b) ~> a) ~> a ~> (b ~> c ~> b) ~> a
, prove $ a ~> (((a ~> a ~> b) ~> c ~> b) ~> (a ~> a ~> b) ~> c ~> b) ~> (a ~> a ~> b) ~> c ~> b
, prove $ (a ~> a ~> (a ~> b ~> c) ~> b) ~> a ~> (a ~> b ~> c) ~> c
, prove $ a ~> ((a ~> a ~> b ~> c) ~> b) ~> (a ~> a ~> b ~> c) ~> c
, prove $ a ~> ((a ~> a ~> b ~> c) ~> b) ~> (a ~> a ~> b ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> b) ~> (a ~> a ~> b) ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> c ~> (b ~> (a ~> a ~> b) ~> d) ~> d
, prove $ (a ~> a ~> (a ~> b ~> c) ~> b) ~> (a ~> b ~> c) ~> a ~> c
, prove $ (a ~> a ~> ((a ~> b) ~> c) ~> b) ~> ((a ~> b) ~> c) ~> c
, prove $ (a ~> a ~> a ~> (b ~> c) ~> b) ~> a ~> (b ~> c) ~> c
, prove $ a ~> (a ~> (a ~> b ~> c) ~> b) ~> (a ~> b ~> c) ~> c
, prove $ (a ~> a ~> ((a ~> b) ~> c) ~> b) ~> ((a ~> b) ~> c) ~> d ~> c
, prove $ a ~> (a ~> (a ~> b ~> c) ~> b) ~> (a ~> b ~> c) ~> d ~> c
, prove $ (((a ~> a) ~> a) ~> b ~> c) ~> b ~> a ~> c
, prove $ (a ~> a ~> a ~> b ~> c) ~> b ~> a ~> c
, prove $ (a ~> a) ~> (a ~> b ~> c) ~> b ~> a ~> c
, prove $ (a ~> a ~> a ~> b ~> c) ~> b ~> a ~> d ~> c
, prove $ a ~> (((a ~> a ~> b) ~> c ~> b) ~> a ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> b) ~> c ~> b) ~> a ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> c ~> b) ~> a ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> b) ~> a ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> c ~> (b ~> a ~> d) ~> d
, prove $ a ~> (a ~> a ~> b ~> c) ~> b ~> b
, prove $ a ~> (a ~> a ~> b) ~> c ~> (b ~> b) ~> b
, prove $ (a ~> a ~> a ~> (b ~> c) ~> b) ~> (b ~> c) ~> a ~> c
, prove $ a ~> (a ~> a ~> (b ~> c) ~> b) ~> (b ~> c) ~> c
, prove $ a ~> (a ~> a ~> (b ~> c) ~> b) ~> (b ~> c) ~> d ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> b ~> c
, prove $ a ~> (a ~> a ~> (b ~> c) ~> (b ~> c) ~> b) ~> (b ~> c) ~> c
, prove $ a ~> a ~> (a ~> b ~> c) ~> ((b ~> c) ~> b) ~> c
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> b) ~> c ~> b) ~> c ~> b
, prove $ a ~> (a ~> a ~> b ~> c) ~> ((b ~> c) ~> c) ~> c
, prove $ ((a ~> (a ~> a ~> b ~> c) ~> b ~> c) ~> d) ~> d
, prove $ a ~> (((a ~> a ~> b ~> c) ~> b ~> c) ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> b ~> c) ~> b ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> ((b ~> c) ~> b ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> b ~> c) ~> ((b ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> b ~> c) ~> b ~> (c ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> c ~> (b ~> c ~> d) ~> d
, prove $ a ~> ((a ~> a ~> b ~> c) ~> b) ~> d ~> (a ~> a ~> b ~> c) ~> c
, prove $ a ~> ((a ~> a ~> b) ~> (c ~> b) ~> d) ~> (a ~> a ~> b) ~> d
, prove $ (a ~> a ~> ((a ~> b) ~> c) ~> b) ~> d ~> ((a ~> b) ~> c) ~> c
, prove $ a ~> (a ~> (a ~> b ~> c) ~> b) ~> d ~> (a ~> b ~> c) ~> c
, prove $ a ~> (a ~> (a ~> b) ~> (c ~> b) ~> d) ~> (a ~> b) ~> d
, prove $ (a ~> a ~> a ~> b ~> c) ~> b ~> d ~> a ~> c
, prove $ (((a ~> a ~> a ~> b) ~> c ~> b) ~> d) ~> a ~> d
, prove $ (a ~> ((a ~> a ~> b) ~> c ~> b) ~> d) ~> a ~> d
, prove $ (a ~> a ~> ((a ~> b) ~> c ~> b) ~> d) ~> a ~> d
, prove $ (a ~> a ~> a ~> (b ~> c ~> b) ~> d) ~> a ~> d
, prove $ (a ~> a ~> a ~> b) ~> ((c ~> b) ~> d) ~> a ~> d
, prove $ (a ~> a ~> a ~> b) ~> c ~> (b ~> d) ~> a ~> d
, prove $ a ~> (a ~> a ~> (b ~> c) ~> b) ~> d ~> (b ~> c) ~> c
, prove $ a ~> (a ~> a ~> b ~> (c ~> b) ~> d) ~> b ~> d
, prove $ a ~> (a ~> a ~> b ~> c) ~> b ~> d ~> c
, prove $ a ~> (a ~> a ~> b) ~> (c ~> b ~> d) ~> c ~> d
, prove $ ((a ~> (a ~> a ~> b) ~> c ~> b) ~> d) ~> d
, prove $ a ~> (((a ~> a ~> b) ~> c ~> b) ~> d) ~> d
, prove $ a ~> (a ~> ((a ~> b) ~> c ~> b) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> c ~> b) ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> b) ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> c ~> (b ~> d) ~> d
, prove $ a ~> (a ~> a ~> b ~> c) ~> b ~> d ~> e ~> c
, prove $ ((a ~> (a ~> a ~> b) ~> c ~> b) ~> d) ~> e ~> d
, prove $ a ~> (((a ~> a ~> b) ~> c ~> b) ~> d) ~> e ~> d
, prove $ a ~> (a ~> ((a ~> b) ~> c ~> b) ~> d) ~> e ~> d
, prove $ a ~> (a ~> a ~> (b ~> c ~> b) ~> d) ~> e ~> d
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> b) ~> d) ~> e ~> d
, prove $ a ~> (a ~> a ~> b) ~> c ~> (b ~> d) ~> e ~> d
, prove $ (a ~> a ~> a ~> b) ~> c ~> c
, prove $ (a ~> a) ~> a ~> b ~> c ~> c
, prove $ a ~> (a ~> a ~> b) ~> c ~> c
, prove $ a ~> (a ~> a) ~> b ~> c ~> c
, prove $ a ~> (a ~> a ~> (b ~> c ~> c) ~> a) ~> a ~> (b ~> c ~> c) ~> a
, prove $ (((a ~> a) ~> a) ~> b) ~> ((c ~> c) ~> a) ~> b
, prove $ (((a ~> a) ~> a) ~> b) ~> c ~> (c ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> ((c ~> c) ~> a) ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> c ~> (c ~> a) ~> b
, prove $ a ~> (a ~> a ~> (b ~> c ~> c) ~> a ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> ((c ~> c) ~> b ~> d) ~> d
, prove $ a ~> (a ~> a ~> b) ~> c ~> (c ~> b ~> d) ~> d
, prove $ (a ~> a ~> a ~> (b ~> c ~> c) ~> d) ~> a ~> d
, prove $ ((a ~> (a ~> a ~> b ~> c) ~> c) ~> d) ~> b ~> d
, prove $ a ~> (((a ~> a ~> b ~> c) ~> c) ~> d) ~> b ~> d
, prove $ a ~> (a ~> ((a ~> b ~> c) ~> c) ~> d) ~> b ~> d
, prove $ a ~> (a ~> a ~> ((b ~> c) ~> c) ~> d) ~> b ~> d
, prove $ a ~> (a ~> a ~> b ~> (c ~> c) ~> d) ~> b ~> d
, prove $ a ~> (a ~> a ~> b ~> c) ~> (c ~> d) ~> b ~> d
, prove $ a ~> (a ~> a ~> (b ~> c) ~> c ~> d) ~> c ~> d
, prove $ a ~> (a ~> a ~> (b ~> c ~> c) ~> d) ~> d
, prove $ a ~> (a ~> a ~> (b ~> c ~> c) ~> d) ~> e ~> d
, prove $ ((a ~> a) ~> a) ~> b ~> c ~> d ~> a
, prove $ (a ~> a) ~> a ~> b ~> c ~> d ~> a
, prove $ a ~> (a ~> a ~> b) ~> c ~> d ~> a
, prove $ a ~> (a ~> a) ~> b ~> c ~> d ~> a
, prove $ ((a ~> a) ~> a) ~> b ~> c ~> d ~> (a ~> a) ~> a
, prove $ (a ~> a ~> a) ~> b ~> c ~> d ~> a ~> a ~> a
, prove $ a ~> (a ~> a ~> b) ~> c ~> d ~> a ~> a ~> b
, prove $ a ~> (a ~> a ~> b ~> c) ~> ((d ~> a ~> a ~> b ~> c) ~> b) ~> c
, prove $ a ~> (a ~> a ~> b ~> c) ~> d ~> ((a ~> a ~> b ~> c) ~> b) ~> c
, prove $ a ~> (a ~> a ~> (b ~> c) ~> d) ~> ((a ~> a ~> (b ~> c) ~> d) ~> c) ~> d
, prove $ (((a ~> a) ~> a) ~> b) ~> c ~> d ~> a ~> b
, prove $ (a ~> a ~> a ~> b) ~> c ~> d ~> a ~> b
, prove $ (a ~> a) ~> (a ~> b) ~> c ~> d ~> a ~> b
, prove $ (a ~> a ~> a ~> b ~> c)