---

Step * 1 of Lemma tree2fun_wf


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
BY
{ ((GenConclTerm ⌜g y⌝⋅ THENA Auto) THEN (CallByValueReduce 0 THENA Auto) THEN BackThruSomeHyp) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  eq  :  EqDecider(A)
5.  value-type(B)
6.  y  :  A
7.  f  :  B  {}\mrightarrow{}  W(C  +  A;a.case  a  of  inl(n)  =>  Void  |  inr(m)  =>  B)
8.  \mforall{}b:B.  \mforall{}g:A  {}\mrightarrow{}  B.    (tree2fun(eq;f  b;g)  \mmember{}  C)
9.  g  :  A  {}\mrightarrow{}  B@i
\mvdash{}  eval  x  =  g  y  in
    tree2fun(eq;f  x;\mlambda{}i.if  eq  i  y  then  x  else  g  i  fi  )  \mmember{}  C


By

---

Latex:
((GenConclTerm  \mkleeneopen{}g  y\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (CallByValueReduce  0  THENA  Auto)  THEN  BackThruSomeHyp)

---

Home Index