---

Step * of Lemma norm-union_wf

∀[A,B:Type].
  (∀[Na:id-fun(A)]. ∀[Nb:id-fun(B)].  (norm-union(Na;Nb) ∈ id-fun(A + B))) supposing (value-type(B) and value-type(A))
BY
{ (Auto
   THEN All (Unfold `id-fun`)
   THEN FunExt⋅
   THEN Auto
   THEN Try (ProveWfLemma)
   THEN D -1
   THEN RepUR ``norm-union`` 0
   THEN (GenConclAtAddr [2;1] THEN D -2 THEN CallByValueReduce 0 THEN Auto THEN MemTypeCD THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    (\mforall{}[Na:id-fun(A)].  \mforall{}[Nb:id-fun(B)].    (norm-union(Na;Nb)  \mmember{}  id-fun(A  +  B)))  supposing 
          (value-type(B)  and 
          value-type(A))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `id-fun`)
  THEN  FunExt\mcdot{}
  THEN  Auto
  THEN  Try  (ProveWfLemma)
  THEN  D  -1
  THEN  RepUR  ``norm-union``  0
  THEN  (GenConclAtAddr  [2;1]  THEN  D  -2  THEN  CallByValueReduce  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto)\mcdot{})

---

Home Index