---

Step * 1 1 1 of Lemma wfd_tree_rec_node_lemma


1. F : Top@i
2. f : Top@i
3. F1 : Top@i
4. b : Top@i
⊢ F1[λb@0.W-rec(a,f,r.if a then b else F1[r] fi ;f b@0)] ~ F1[λx.W-rec(a,f,r.if a then b else F1[r] fi ;f x)]
BY
{ Try SqEqCD }

---

Latex:

---

Latex:

1.  F  :  Top@i
2.  f  :  Top@i
3.  F1  :  Top@i
4.  b  :  Top@i
\mvdash{}  F1[\mlambda{}b@0.W-rec(a,f,r.if  a  then  b  else  F1[r]  fi  ;f  b@0)]  \msim{}  F1[\mlambda{}x.W-rec(a,f,r.if  a
                                                                                                                                  then  b
                                                                                                                                  else  F1[r]
                                                                                                                                  fi  ;f  x)]


By

---

Latex:
Try  SqEqCD

---

Home Index