---

Step * of Lemma norm-pair_wf

∀[A:Type]. ∀[B:A ⟶ Type].
  (∀[Na:id-fun(A)]. ∀[Nb:⋂a:A. id-fun(B[a])].  (norm-pair(Na;Nb) ∈ id-fun(a:A × B[a]))) supposing 
     ((∀a:A. value-type(B[a])) and 
     value-type(A))
BY
{ (Auto
   THEN All (Unfold `id-fun`)
   THEN (ExtWith [`p'] [⌜Top ⟶ Top⌝]⋅ THENA Auto)
   THEN D -1
   THEN RepUR ``norm-pair`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (GenConclAtAddr [2;1] THEN D -2 THEN GenConclAtAddr [2;2]⋅ THEN D -2 THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    (\mforall{}[Na:id-fun(A)].  \mforall{}[Nb:\mcap{}a:A.  id-fun(B[a])].    (norm-pair(Na;Nb)  \mmember{}  id-fun(a:A  \mtimes{}  B[a])))  supposing 
          ((\mforall{}a:A.  value-type(B[a]))  and 
          value-type(A))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `id-fun`)
  THEN  (ExtWith  [`p']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RepUR  ``norm-pair``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (GenConclAtAddr  [2;1]  THEN  D  -2  THEN  GenConclAtAddr  [2;2]\mcdot{}  THEN  D  -2  THEN  Auto))

---

Home Index