---

Step * 1 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)
7. [a / as] = [b / bs] ∈ {cs:A List| ||cs|| ≥ 1 } 
⊢ a = b ∈ A
BY
{ (ApFunToHypEquands `z' ⌜hd(z)⌝ ⌜A⌝ 7 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(ApFunToHypEquands  `z'  \mkleeneopen{}hd(z)\mkleeneclose{}  \mkleeneopen{}A\mkleeneclose{}  7  THEN  Auto)

---

Home Index