---

Step * of Lemma pi-comp_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[B:{Gamma.A ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[cB:Gamma.A ⊢ CompOp(B)].
  (pi-comp(Gamma;A;B;cA;cB) ∈ Gamma ⊢ CompOp(ΠA B))
BY
{ (Intros THEN MemTypeCD THEN Try ((RepeatFor 6 ((FunExt THENA Auto)) THEN MemTypeCD)) THEN Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[B:\{Gamma.A  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  CompOp(A)].
\mforall{}[cB:Gamma.A  \mvdash{}  CompOp(B)].
    (pi-comp(Gamma;A;B;cA;cB)  \mmember{}  Gamma  \mvdash{}  CompOp(\mPi{}A  B))


By

---

Latex:
(Intros
  THEN  MemTypeCD
  THEN  Try  ((RepeatFor  6  ((FunExt  THENA  Auto))  THEN  MemTypeCD))
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index