---

Step * of Lemma cons_functionality_wrt_permr

∀T:Type. ∀a,b:T. ∀as,bs:T List.  ((a = b ∈ T) ⇒ (as ≡(T) bs) ⇒ ([a / as] ≡(T) [b / bs]))
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. a : T
3. b : T
4. as : T List
5. bs : T List
6. a = b ∈ T
7. as ≡(T) bs
⊢ [a / as] ≡(T) [b / bs]

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}a,b:T.  \mforall{}as,bs:T  List.    ((a  =  b)  {}\mRightarrow{}  (as  \mequiv{}(T)  bs)  {}\mRightarrow{}  ([a  /  as]  \mequiv{}(T)  [b  /  bs]))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index