test.hs

dgp :: Formula -> Formula -> Formula
dgp p q = (p #> q) #| (q #> p)

pp :: Formula -> Formula -> Formula
pp p q = ((p #> q) #> p) #> p

p = Proposition "P"
q = Proposition "Q"
r = (dgp p q) #> p
s = pp (dgp p q) p

test = do
    dQ        <- assume q
    dPtoQ     <- implIntro p dQ
    dDGP''    <- rightDisjIntro (q #> p) dPtoQ
    dDGPtoP   <- assume r
    dP        <- implElim dDGP dDGPtoP
    dQtoP     <- implIntro q dP
    dDGP'     <- leftDisjIntro (p #> q) dQtoP
    dRtoDGP'  <- implIntro r dDGP'
    dPP       <- assume s
    implElim dPP dRtoDGP'
    
-- a proof that ((((p -> q) v (q -> p)) -> p) -> ((p -> q) v (q -> p))) -> ((p -> q) v (q -> p))
--                                          implies
--                                    (p -> q) v (q -> p)
-- in minimal logic