---

Step * of Lemma cubical-type-restriction-and

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}]. ∀[psi,phi:I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ].
  (cubical-type-restriction(X;T;I,a,t.psi[I;a;t])
  ⇒ cubical-type-restriction(X;T;I,a,t.phi[I;a;t])
  ⇒ cubical-type-restriction(X;T;I,a,t.psi[I;a;t] ∧ phi[I;a;t]))
BY
{ (Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{X  \mvdash{}  \_\}].  \mforall{}[psi,phi:I:fset(\mBbbN{})  {}\mrightarrow{}  alpha:X(I)  {}\mrightarrow{}  T(alpha)  {}\mrightarrow{}  \mBbbP{}].
    (cubical-type-restriction(X;T;I,a,t.psi[I;a;t])
    {}\mRightarrow{}  cubical-type-restriction(X;T;I,a,t.phi[I;a;t])
    {}\mRightarrow{}  cubical-type-restriction(X;T;I,a,t.psi[I;a;t]  \mwedge{}  phi[I;a;t]))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index