---

Step * of Lemma discrete-fun-app-invariant

∀[A,B:Type]. ∀[f:{() ⊢ _:(discr(A) ⟶ discr(B))}]. ∀[I:fset(ℕ)]. ∀[a:()(I)]. ∀[t:A].
  (app(f; discr(t))(a) = app(f; discr(t))(⋅) ∈ B)
BY
{ (Unfold `cubical-term-at` 0 THEN InstLemma `discrete-fun-invariant` [] THEN RepeatFor 5 (ParallelLast') THEN Intros) }

1
1. A : Type
2. B : Type
3. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
4. I : fset(ℕ)
5. a : ()(I)
6. (f I a) = (f {} ⋅) ∈ (discr(A) ⟶ discr(B))(a)
7. t : A
⊢ (app(f; discr(t)) I a) = (app(f; discr(t)) {} ⋅) ∈ B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:\{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:()(I)].  \mforall{}[t:A].
    (app(f;  discr(t))(a)  =  app(f;  discr(t))(\mcdot{}))


By

---

Latex:
(Unfold  `cubical-term-at`  0
  THEN  InstLemma  `discrete-fun-invariant`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  Intros)

---

Home Index