---

Step * 1 of Lemma eq_cons_imp_eq_hds


1. A : Type
2. a : A
3. b : A
4. as : A List
5. bs : A List
6. [a / as] = [b / bs] ∈ (A List)
⊢ a = b ∈ A
BY
{ (Assert ⌜[a / as] = [b / bs] ∈ {cs:A List| ||cs|| ≥ 1 } ⌝ THENA Auto) }

1
1. A : Type
2. a : A
3. b : A
4. as : A List
5. bs : A List
6. [a / as] = [b / bs] ∈ (A List)
7. [a / as] = [b / bs] ∈ {cs:A List| ||cs|| ≥ 1 } 
⊢ a = b ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  a  :  A
3.  b  :  A
4.  as  :  A  List
5.  bs  :  A  List
6.  [a  /  as]  =  [b  /  bs]
\mvdash{}  a  =  b


By

---

Latex:
(Assert  \mkleeneopen{}[a  /  as]  =  [b  /  bs]\mkleeneclose{}  THENA  Auto)

---

Home Index