---

Step * of Lemma implies-vdf-eq-append1

No Annotations
∀A,B:Type. ∀C:A ⟶ B ⟶ Type. ∀f:very-dep-fun(A;B;a,b.C[a;b]). ∀L:(a:A × b:B × C[a;b]) List. ∀a:A. ∀b:B. ∀c:Top.
  (vdf-eq(A;f;L) ⇒ (a = (f L b) ∈ A) ⇒ vdf-eq(A;f;L @ [<a, b, c>]))
BY
{ (InstLemma `very-dep-fun-subtype` []⋅
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN (RWO "vdf-eq-append1" 0 THENA Auto)
   THEN UseWitness ⌜Ax⌝⋅
   THEN DepIsectCD
   THEN ((BLemma `vdf-eq-witness` THEN Auto) ORELSE (MemCD THEN Auto))) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}A,B:Type.  \mforall{}C:A  {}\mrightarrow{}  B  {}\mrightarrow{}  Type.  \mforall{}f:very-dep-fun(A;B;a,b.C[a;b]).  \mforall{}L:(a:A  \mtimes{}  b:B  \mtimes{}  C[a;b])  List.  \mforall{}a:A.
\mforall{}b:B.  \mforall{}c:Top.
    (vdf-eq(A;f;L)  {}\mRightarrow{}  (a  =  (f  L  b))  {}\mRightarrow{}  vdf-eq(A;f;L  @  [<a,  b,  c>]))


By

---

Latex:
(InstLemma  `very-dep-fun-subtype`  []\mcdot{}
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  (RWO  "vdf-eq-append1"  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  DepIsectCD
  THEN  ((BLemma  `vdf-eq-witness`  THEN  Auto)  ORELSE  (MemCD  THEN  Auto)))

---

Home Index