---

Step * of Lemma apply-wf-per

∀[A:Type]. ∀[B:type-function{i:l}(A)]. ∀[f:per-function(A;a.B[a])]. ∀[a:A].  (f[a] ∈ B[a])
BY
{ (Intros
   THEN InstLemma `per-function_wf`[⌜A⌝;⌜B⌝]⋅
   THEN Auto
   THEN Unhide
   THEN PointwiseFunctionality 3
   THEN Try ((EqCD THEN Auto)⋅)
   THEN Try (Unhide)
   THEN (PerHD (-3)⋅
         THEN InstLemma `function-eq_wf_type_function` [⌜A⌝;⌜B⌝]⋅
         THEN Auto
         THEN (At ⌜Type⌝ (PointwiseFunctionality 7)⋅
               THEN (Assert ⌜(B a2) = (B b1) ∈ Type⌝⋅ THEN Auto)⋅
               THEN All (Unfolds ``so_apply function-eq member``)
               THEN Try ((EqCD THEN Auto))
               THEN Try ((InstHyp [⌜a2⌝;⌜a2⌝] 6⋅ THEN Auto)⋅)
               THEN Try ((InstHyp [⌜b1⌝;⌜b1⌝] 6⋅ THEN Auto)⋅)
               THEN Try ((InstHyp [⌜a2⌝;⌜b1⌝] 6⋅ THEN Auto)⋅))⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:type-function\{i:l\}(A)].  \mforall{}[f:per-function(A;a.B[a])].  \mforall{}[a:A].    (f[a]  \mmember{}  B[a])


By

---

Latex:
(Intros
  THEN  InstLemma  `per-function\_wf`[\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Unhide
  THEN  PointwiseFunctionality  3
  THEN  Try  ((EqCD  THEN  Auto)\mcdot{})
  THEN  Try  (Unhide)
  THEN  (PerHD  (-3)\mcdot{}
              THEN  InstLemma  `function-eq\_wf\_type\_function`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}
              THEN  Auto
              THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (PointwiseFunctionality  7)\mcdot{}
                          THEN  (Assert  \mkleeneopen{}(B  a2)  =  (B  b1)\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}
                          THEN  All  (Unfolds  ``so\_apply  function-eq  member``)
                          THEN  Try  ((EqCD  THEN  Auto))
                          THEN  Try  ((InstHyp  [\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{}]  6\mcdot{}  THEN  Auto)\mcdot{})
                          THEN  Try  ((InstHyp  [\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]  6\mcdot{}  THEN  Auto)\mcdot{})
                          THEN  Try  ((InstHyp  [\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]  6\mcdot{}  THEN  Auto)\mcdot{}))\mcdot{})\mcdot{})

---

Home Index