---

Step * 1 of Lemma vdf-eq-append1


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
BY
{ ((Subst' L @ [<a, b, c>][||L||] ~ <a, b, c> -1 THENA ((RWO "select-append" 0 THENA Auto) THEN Subst' ||L|| - ||L|| ~ 0\000C 0 THEN Reduce 0 THEN Auto))
   THEN RepUR ``let`` -1
   THEN NthHypSq (-1)
   THEN Auto
   THEN Try (((RWO "firstn-append" 0 THENA Auto) THEN AutoSplit))
   THEN RWO "firstn_all" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  Top
3.  L  :  (a:Top  \mtimes{}  b:Top  \mtimes{}  Top)  List
4.  a  :  Top
5.  b  :  Top
6.  c  :  Top
7.  vdf-eq(A;f;firstn(||L||  +  1;L  @  [<a,  b,  c>])) 
\msim{}  x:vdf-eq(A;f;firstn(||L||;L  @  [<a,  b,  c>]))  \mcap{}  let  tr  =  L  @  [<a,  b,  c>][||L||]  in
                                                                                                      (fst(tr))
                                                                                                      =  (f  firstn(||L||;L  @  [<a,  b,  c>])  (fst(snd(tr)))\000C)
\mvdash{}  vdf-eq(A;f;L  @  [<a,  b,  c>])  \msim{}  x:vdf-eq(A;f;L)  \mcap{}  a  =  (f  L  b)


By

---

Latex:
((Subst'  L  @  [<a,  b,  c>][||L||]  \msim{}  <a,  b,  c>  -1
    THENA  ((RWO  "select-append"  0  THENA  Auto)  THEN  Subst'  ||L||  -  ||L||  \msim{}  0  0  THEN  Reduce  0  THEN  Auto)
    )
  THEN  RepUR  ``let``  -1
  THEN  NthHypSq  (-1)
  THEN  Auto
  THEN  Try  (((RWO  "firstn-append"  0  THENA  Auto)  THEN  AutoSplit))
  THEN  RWO  "firstn\_all"  0
  THEN  Auto)

---

Home Index