---

Step * of Lemma rev-type-comp_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ Compositon(A)].  (rev-type-comp(Gamma;cA) ∈ Gamma.𝕀 ⊢ Compositon((A)-))
BY
{ ((Intros THEN (Assert 1-(q) ∈ {Gamma.𝕀 ⊢ _:(𝕀)p} BY (SubsumeC ⌜{Gamma.𝕀 ⊢ _:𝕀}⌝⋅ THEN Auto)))
   THEN (InstLemma `csm-comp-structure_wf` [⌜Gamma.𝕀⌝;⌜Gamma.𝕀⌝;⌜(p;1-(q))⌝;⌜A⌝;⌜cA⌝]⋅ THENA Auto)
   THEN Folds ``rev-type-line rev-type-comp`` (-1)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  Compositon(A)].
    (rev-type-comp(Gamma;cA)  \mmember{}  Gamma.\mBbbI{}  \mvdash{}  Compositon((A)-))


By

---

Latex:
((Intros  THEN  (Assert  1-(q)  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:(\mBbbI{})p\}  BY  (SubsumeC  \mkleeneopen{}\{Gamma.\mBbbI{}  \mvdash{}  \_:\mBbbI{}\}\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  (InstLemma  `csm-comp-structure\_wf`  [\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}(p;1-(q))\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}cA\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Folds  ``rev-type-line  rev-type-comp``  (-1)
  THEN  Auto)

---

Home Index