---

Step * of Lemma tree2fun_wf

∀[A,B,C:Type]. ∀[eq:EqDecider(A)].  ∀[w:type2tree(A;B;C)]. ∀[g:A ⟶ B].  (tree2fun(eq;w;g) ∈ C) supposing value-type(B)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN UnfoldTopAb (-1)
   THEN WElim (-1)
   THEN ((Auto THEN Unfold `tree2fun` 0) THEN RepUR ``Wsup`` 0)
   THEN DVar `a'
   THEN All Reduce
   THEN Try (Trivial)) }

1
1. A : Type
2. B : Type
3. C : Type
4. eq : EqDecider(A)
5. value-type(B)
6. y : A
7. f : B ⟶ W(C + A;a.case a of inl(n) => Void | inr(m) => B)
8. ∀b:B. ∀g:A ⟶ B.  (tree2fun(eq;f b;g) ∈ C)
9. g : A ⟶ B@i
⊢ eval x = g y in
  tree2fun(eq;f x;λi.if eq i y then x else g i fi ) ∈ C

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[eq:EqDecider(A)].
    \mforall{}[w:type2tree(A;B;C)].  \mforall{}[g:A  {}\mrightarrow{}  B].    (tree2fun(eq;w;g)  \mmember{}  C)  supposing  value-type(B)


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  UnfoldTopAb  (-1)
  THEN  WElim  (-1)
  THEN  ((Auto  THEN  Unfold  `tree2fun`  0)  THEN  RepUR  ``Wsup``  0)
  THEN  DVar  `a'
  THEN  All  Reduce
  THEN  Try  (Trivial))

---

Home Index