module HomeworkFifteen
%default total

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

data Et : Term -> Type where
  ETru : Et Tru
  EFls : Et (Not Fls)
  ENot : Et t -> Et (Not (Not t))
  ECondT : Et tc -> Et tt -> Et (Cond tc tt te)
  ECondF : Et (Not tc) -> Et te -> Et (Cond tc tt te)

ex1 : Et (Not (Not (Not Fls)))
ex1 = ENot EFls

ex2 : Et (Cond Tru (Not Fls) Tru)
ex2 = ECondT ETru EFls

ex3 : Et (Cond Fls Fls Tru)
ex3 = ECondF EFls ETru

infixl 5 !!

data (!!) : Term -> Term -> Type where
  STru : Tru !! Tru
  SFls : Fls !! Fls
  SNotT : t !! Tru -> Not t !! Fls
  SNotF : t !! Fls -> Not t !! Tru
  SCondT : tc !! Tru -> tt !! v -> (Cond tc tt te) !! v
  SCondF : tc !! Fls -> te !! v -> (Cond tc tt te) !! v

lemma : Et t -> t !! Tru
lemma ETru = STru
lemma EFls = SNotF SFls
lemma (ENot e) = SNotF $ SNotT $ lemma e
lemma (ECondT c t) = SCondT (lemma c) (lemma t)
lemma (ECondF c e) with (lemma c)
  | SNotF pc = SCondF pc (lemma e)

lemma' : t !! Tru -> Et t
lemma' STru = ETru
lemma' (SNotF f) = ?stuckHere
lemma' (SCondT tc tt) = ECondT (lemma' tc) (lemma' tt)
lemma' (SCondF tc te) = ECondF (lemma' $ SNotF tc) (lemma' te)