---

Step * 1 1 of Lemma per-or-equal

.....subterm..... T:t
2:n
1. A1 : Type
2. B1 : Type
3. A2 : Type
4. B2 : Type
5. B1 ≡ B2
6. A1 ≡ A2
7. x : Base
8. y : Base
9. (fst(x)) = (fst(y)) ∈ per-value()
⊢ (snd(x)) = (snd(y)) ∈ if fst(x) = Ax then A1 otherwise B1 ∈ Type
BY
{ (BLemma `equal-wf-base`
   THEN Auto
   THEN (InstLemma `per-value-property` [⌜fst(x)⌝]⋅ THENA Auto)
   THEN DUand (-1)
   THEN CanonicalAuto)⋅ }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  A1  :  Type
2.  B1  :  Type
3.  A2  :  Type
4.  B2  :  Type
5.  B1  \mequiv{}  B2
6.  A1  \mequiv{}  A2
7.  x  :  Base
8.  y  :  Base
9.  (fst(x))  =  (fst(y))
\mvdash{}  (snd(x))  =  (snd(y))  \mmember{}  Type


By

---

Latex:
(BLemma  `equal-wf-base`
  THEN  Auto
  THEN  (InstLemma  `per-value-property`  [\mkleeneopen{}fst(x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DUand  (-1)
  THEN  CanonicalAuto)\mcdot{}

---

Home Index