module Ex2 where
import Prop
import Examples
import Tactics
import HR

p = LetterP "p"
q = LetterP "q"
r = LetterP "r"

lhs = ImpliesP p (ImpliesP q r)
rhs = ImpliesP (AndP p q) r

goal = Sequent [lhs] rhs

proof = prove goal [impliesI, impliesE q, impliesE p, hypothesis, andE1 q, hypothesis, andE2 p, hypothesis]

animation = replay goal [impliesI, impliesE q, impliesE p, hypothesis, andE1 q, hypothesis, andE2 p, hypothesis]