---

Step * of Lemma norm-pair_wf_sq

∀[A,B:Type].
  (∀[Na:sq-id-fun(A)]. ∀[Nb:sq-id-fun(B)].  (norm-pair(Na;Nb) ∈ sq-id-fun(A × B))) supposing 
     ((B ⊆r Base) and 
     (A ⊆r Base) and 
     value-type(B) and 
     value-type(A))
BY
{ (Auto
   THEN (Assert SQType(A) BY
               SqTac)
   THEN (Assert SQType(B) BY
               SqTac)
   THEN All (Unfold `sq-id-fun`)
   THEN All (Unfold `sqequal`)
   THEN FunExt⋅
   THEN Auto
   THEN Try (ProveWfLemma)
   THEN D -1
   THEN RepUR ``norm-pair`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0⋅ THENA Auto))) }

1
1. A : Type
2. B : Type
3. value-type(A)
4. value-type(B)
5. A ⊆r Base
6. B ⊆r Base
7. Na : x:A ⟶ {y:A| x ~ y} 
8. Nb : x:B ⟶ {y:B| x ~ y} 
9. SQType(A)
10. SQType(B)
11. x1 : A
12. x2 : B
⊢ <Na x1, Nb x2> ∈ {y:A × B| <x1, x2> ~ y} 

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    (\mforall{}[Na:sq-id-fun(A)].  \mforall{}[Nb:sq-id-fun(B)].    (norm-pair(Na;Nb)  \mmember{}  sq-id-fun(A  \mtimes{}  B)))  supposing 
          ((B  \msubseteq{}r  Base)  and 
          (A  \msubseteq{}r  Base)  and 
          value-type(B)  and 
          value-type(A))


By

---

Latex:
(Auto
  THEN  (Assert  SQType(A)  BY
                          SqTac)
  THEN  (Assert  SQType(B)  BY
                          SqTac)
  THEN  All  (Unfold  `sq-id-fun`)
  THEN  All  (Unfold  `sqequal`)
  THEN  FunExt\mcdot{}
  THEN  Auto
  THEN  Try  (ProveWfLemma)
  THEN  D  -1
  THEN  RepUR  ``norm-pair``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0\mcdot{}  THENA  Auto)))

---

Home Index