---

Step * of Lemma param-W-ext

∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
  pW ≡ λp.(a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b])))
BY
{ TACTIC:(Auto
          THEN InstLemma `param-co-W_wf` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝]⋅
          THEN Auto
          THEN RepeatFor 2 ((D 0 THEN Auto))
          THEN Reduce 0
          THEN At ⌜Type⌝ (D 0)⋅
          THEN Auto) }

1
.....subterm..... T:t
1:n
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. p : P
7. x : pW p
⊢ x ∈ a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b]))

2
.....subterm..... T:t
1:n
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. p : P
7. x : a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b]))
⊢ x ∈ pW p

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[A:P  {}\mrightarrow{}  Type].  \mforall{}[B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type].  \mforall{}[C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P].
    pW  \mequiv{}  \mlambda{}p.(a:A[p]  \mtimes{}  (b:B[p;a]  {}\mrightarrow{}  (pW  C[p;a;b])))


By

---

Latex:
TACTIC:(Auto
                THEN  InstLemma  `param-co-W\_wf`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  RepeatFor  2  ((D  0  THEN  Auto))
                THEN  Reduce  0
                THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto)

---

Home Index