---

Step * 1 of Lemma norm-fst_wf


1. A : Type
2. B : A ⟶ Type
3. value-type(A)
4. N : x:A ⟶ {y:A| x = y ∈ A} 
5. a : A
6. x1 : B[a]
⊢ x1 ∈ B[N a]
BY
{ (DoSubsume
   THEN Try (BLemma `subtype_rel-equal`)
   THEN Auto
   THEN (EqCD THEN Auto THEN GenConclAtAddr [3] THEN D (-2)⋅ THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  value-type(A)
4.  N  :  x:A  {}\mrightarrow{}  \{y:A|  x  =  y\} 
5.  a  :  A
6.  x1  :  B[a]
\mvdash{}  x1  \mmember{}  B[N  a]


By

---

Latex:
(DoSubsume
  THEN  Try  (BLemma  `subtype\_rel-equal`)
  THEN  Auto
  THEN  (EqCD  THEN  Auto  THEN  GenConclAtAddr  [3]  THEN  D  (-2)\mcdot{}  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index