---

Step * 1 1 of Lemma id-sdata-one-one


1. a : Id
2. b : Id
3. tree_leaf(inl a) = tree_leaf(inl b) ∈ tree(Id + Atom1)
⊢ a = b ∈ Id
BY
{ (ApFunToHypEquands `Z' ⌈if tree_leaf?(Z) then tree_leaf-value(Z) else inl a fi ⌉ ⌈Id + Atom1⌉ (-1)⋅
   THEN Auto
   THEN Reduce (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  Id
2.  b  :  Id
3.  tree\_leaf(inl  a)  =  tree\_leaf(inl  b)
\mvdash{}  a  =  b


By

---

Latex:
(ApFunToHypEquands  `Z'  \mkleeneopen{}if  tree\_leaf?(Z)  then  tree\_leaf-value(Z)  else  inl  a  fi  \mkleeneclose{}  \mkleeneopen{}Id  +  Atom1\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index