---

Step * of Lemma bool-negation-equiv_wf

bool-negation-equiv(()) ∈ {() ⊢ _:Equiv(decode(Bool);decode(Bool))}
BY
{ (Auto
   THEN (Assert bool-negation-equiv(()) ∈ {() ⊢ _:Equiv(discr(𝔹);discr(𝔹))} BY
               ProveWfLemma)
   THEN InferEqualType
   THEN Try (Trivial)
   THEN RepeatFor 2 (EqCDA)
   THEN Auto) }

1
.....subterm..... T:t
2:n
1. bool-negation-equiv(()) ∈ {() ⊢ _:Equiv(discr(𝔹);discr(𝔹))}
⊢ discr(𝔹) = decode(Bool) ∈ {() ⊢ _}

---

Latex:

---

Latex:
bool-negation-equiv(())  \mmember{}  \{()  \mvdash{}  \_:Equiv(decode(Bool);decode(Bool))\}


By

---

Latex:
(Auto
  THEN  (Assert  bool-negation-equiv(())  \mmember{}  \{()  \mvdash{}  \_:Equiv(discr(\mBbbB{});discr(\mBbbB{}))\}  BY
                          ProveWfLemma)
  THEN  InferEqualType
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  (EqCDA)
  THEN  Auto)

---

Home Index