module HomeworkSix
%default total

data Term = Tru | Fls | Not Term | Cond Term Term Term 

data OT : Term -> Type where
  OptNotNot : OT (Not (Not t))
  OptNot : OT t -> OT (Not t)
  OptCond1 : OT t1 -> OT (Cond t1 t2 t3)
  OptCond2 : OT t2 -> OT (Cond t1 t2 t3)
  OptCond3 : OT t3 -> OT (Cond t1 t2 t3)

p1 : OT (Cond (Not Tru) (Not (Not Tru)) Fls)
p1 = OptCond2 OptNotNot

p2 : OT (Not (Not (Not Fls)))
p2 = OptNotNot

p3 : OT (Not (Cond (Not Tru) (Not (Not Tru)) Fls))
p3 = OptNot p1