---

Step * of Lemma fun-comp_wf

No Annotations
∀[Gamma:j⊢]. ∀[A,B:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[cB:Gamma ⊢ CompOp(B)].
  (fun-comp(Gamma; A; B; cA; cB) ∈ Gamma ⊢ CompOp((A ⟶ B)))
BY
{ (Intros
   THEN Unhide
   THEN (InstLemma `pi-comp_wf` [⌜Gamma⌝;⌜A⌝;⌜(B)p⌝;⌜cA⌝;⌜(cB)p⌝]⋅ THENA Auto)
   THEN Fold `fun-comp` (-1)
   THEN InferEqualTypeGen
   THEN EqCDA
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (InstLemma  `pi-comp\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}(B)p\mkleeneclose{};\mkleeneopen{}cA\mkleeneclose{};\mkleeneopen{}(cB)p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `fun-comp`  (-1)
  THEN  InferEqualTypeGen
  THEN  EqCDA
  THEN  Auto)

---

Home Index