---

Step * of Lemma union-list2-simplify1

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ll:T List List]. ∀[L:T List].
  (union-list2(eq;[L; [L / ll]]) ~ union-list2(eq;[L / ll]))
BY
{ ((UnivCD THENA Auto) THEN Subst' union-list2(eq;[L; [L / ll]]) ~ union-list2(eq;[L / ll]) ⋃ L 0) }

1
.....equality..... 
1. T : Type
2. eq : EqDecider(T)
3. ll : T List List
4. L : T List
⊢ union-list2(eq;[L; [L / ll]]) ~ union-list2(eq;[L / ll]) ⋃ L

2
1. T : Type
2. eq : EqDecider(T)
3. ll : T List List
4. L : T List
⊢ union-list2(eq;[L / ll]) ⋃ L ~ union-list2(eq;[L / ll])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[ll:T  List  List].  \mforall{}[L:T  List].
    (union-list2(eq;[L;  [L  /  ll]])  \msim{}  union-list2(eq;[L  /  ll]))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Subst'  union-list2(eq;[L;  [L  /  ll]])  \msim{}  union-list2(eq;[L  /  ll])  \mcup{}  L  0)

---

Home Index