---

Step * of Lemma bar-val_wf

∀[n:ℕ]. ∀[T:Type]. ∀[x:bar-base(T)].  (bar-val(n;x) ∈ T?)
BY
{ (InductionOnNat
   THEN Auto
   THEN RecUnfold
   `bar-val` 0⋅
   THEN Auto
   THEN (GenConcl ⌜x = w ∈ (T + bar-base(T))⌝⋅ THENA (Auto THEN DoSubsume THEN Auto))
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0
   THEN Auto
   THEN InstHyp [⌜T⌝] 3⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[T:Type].  \mforall{}[x:bar-base(T)].    (bar-val(n;x)  \mmember{}  T?)


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  RecUnfold
  `bar-val`  0\mcdot{}
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}x  =  w\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}T\mkleeneclose{}]  3\mcdot{}
  THEN  Auto)

---

Home Index