---

Step * of Lemma sq_stable__vdf-eq

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].
  SqStable(vdf-eq(A;f;L))
BY
{ (Auto THEN (D 0 THENW Auto) THEN D -1 THEN UseWitness ⌜Ax⌝⋅ THEN BLemma `vdf-eq-witness` 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].
    SqStable(vdf-eq(A;f;L))


By

---

Latex:
(Auto  THEN  (D  0  THENW  Auto)  THEN  D  -1  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  BLemma  `vdf-eq-witness`  THEN  Auto)

---

Home Index