---

Step * of Lemma name_eq-normalize

∀[F,G,a,b:Top].  (if name_eq(a;b) then F a else G fi  ~ if name_eq(a;b) then F b else G fi )
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN SqEqualBase
          THEN BLemma  `ifthenelse_sqequal`
          THEN Try (MemBase)
          THEN RepeatFor 2 (D 0)
          THEN Try (Complete (Auto))
          THEN EqCD) }

1
1. G : Base
2. F : Base
3. b : Base
4. a : Base
5. ∃z:Base. (name_eq(a;b) ~ inl z)
⊢ F ~ F

2
1. G : Base
2. F : Base
3. b : Base
4. a : Base
5. ∃z:Base. (name_eq(a;b) ~ inl z)
⊢ a ~ b

---

Latex:

---

Latex:
\mforall{}[F,G,a,b:Top].    (if  name\_eq(a;b)  then  F  a  else  G  fi    \msim{}  if  name\_eq(a;b)  then  F  b  else  G  fi  )


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  SqEqualBase
                THEN  BLemma    `ifthenelse\_sqequal`
                THEN  Try  (MemBase)
                THEN  RepeatFor  2  (D  0)
                THEN  Try  (Complete  (Auto))
                THEN  EqCD)

---

Home Index