Step
*
1
1
of Lemma
map_equal
1. T : Type
2. T' : Type
3. a : T List
4. f : T ⟶ T'
5. g : T ⟶ T'
6. ∀i:ℕ. (i < ||a|| 
⇒ ((f a[i]) = (g a[i]) ∈ T'))
⊢ ||map(f;a)|| = ||map(g;a)|| ∈ ℤ
BY
{ (((InstLemma `map_length` [T;T';f;a] THENA Auto) THEN InstLemma `map_length` [T;T';g;a]) THEN Auto) }
Latex:
Latex:
1.  T  :  Type
2.  T'  :  Type
3.  a  :  T  List
4.  f  :  T  {}\mrightarrow{}  T'
5.  g  :  T  {}\mrightarrow{}  T'
6.  \mforall{}i:\mBbbN{}.  (i  <  ||a||  {}\mRightarrow{}  ((f  a[i])  =  (g  a[i])))
\mvdash{}  ||map(f;a)||  =  ||map(g;a)||
By
Latex:
(((InstLemma  `map\_length`  [T;T';f;a]  THENA  Auto)  THEN  InstLemma  `map\_length`  [T;T';g;a])  THEN  Auto)
Home
Index