---

Step * of Lemma vdf-eq-append1

No Annotations
∀A:Type. ∀f:Top. ∀L:(a:Top × b:Top × Top) List. ∀a,b,c:Top.
  (vdf-eq(A;f;L @ [<a, b, c>]) ~ x:vdf-eq(A;f;L) ⋂ a = (f L b) ∈ A)
BY
{ (Auto THEN (InstLemma `vdf-eq-firstn` [⌜A⌝;⌜f⌝;⌜L @ [<a, b, c>]⌝;⌜||L||⌝]⋅ THENA Auto)) }

1
1. A : Type
2. f : Top
3. L : (a:Top × b:Top × Top) List
4. a : Top
5. b : Top
6. c : Top
7. vdf-eq(A;f;firstn(||L|| + 1;L @ [<a, b, c>])) 
~ x:vdf-eq(A;f;firstn(||L||;L @ [<a, b, c>])) ⋂ let tr = L @ [<a, b, c>][||L||] in
                                                   (fst(tr)) = (f firstn(||L||;L @ [<a, b, c>]) (fst(snd(tr)))) ∈ A
⊢ vdf-eq(A;f;L @ [<a, b, c>]) ~ x:vdf-eq(A;f;L) ⋂ a = (f L b) ∈ A

---

Latex:

---

Latex:
No  Annotations
\mforall{}A:Type.  \mforall{}f:Top.  \mforall{}L:(a:Top  \mtimes{}  b:Top  \mtimes{}  Top)  List.  \mforall{}a,b,c:Top.
    (vdf-eq(A;f;L  @  [<a,  b,  c>])  \msim{}  x:vdf-eq(A;f;L)  \mcap{}  a  =  (f  L  b))


By

---

Latex:
(Auto  THEN  (InstLemma  `vdf-eq-firstn`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}L  @  [<a,  b,  c>]\mkleeneclose{};\mkleeneopen{}||L||\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index