Step * 1 1 1 1 of Lemma set-equal-cons


1. [T] Type
2. T
3. List
4. bs List
5. no_repeats(T;[u v])
6. no_repeats(T;bs)
7. set-equal(T;[u v];bs)
8. (u ∈ bs)
9. l1 List
10. l2 List
11. bs (l1 [u l2]) ∈ (T List)
12. bs (l1 [u l2]) ∈ (T List)
⊢ set-equal(T;v;l1 l2)
BY
(Assert set-equal(T;[u v];l1 [u l2]) BY
         (RevHypSubst (-1) THEN Auto)) }

1
1. [T] Type
2. T
3. List
4. bs List
5. no_repeats(T;[u v])
6. no_repeats(T;bs)
7. set-equal(T;[u v];bs)
8. (u ∈ bs)
9. l1 List
10. l2 List
11. bs (l1 [u l2]) ∈ (T List)
12. bs (l1 [u l2]) ∈ (T List)
13. set-equal(T;[u v];l1 [u l2])
⊢ set-equal(T;v;l1 l2)


Latex:


Latex:

1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
4.  bs  :  T  List
5.  no\_repeats(T;[u  /  v])
6.  no\_repeats(T;bs)
7.  set-equal(T;[u  /  v];bs)
8.  (u  \mmember{}  bs)
9.  l1  :  T  List
10.  l2  :  T  List
11.  bs  =  (l1  @  [u  /  l2])
12.  bs  =  (l1  @  [u  /  l2])
\mvdash{}  set-equal(T;v;l1  @  l2)


By


Latex:
(Assert  set-equal(T;[u  /  v];l1  @  [u  /  l2])  BY
              (RevHypSubst  (-1)  0  THEN  Auto))




Home Index