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