---

Step * 1 1 2 2 1 1 of Lemma polymorphic-choice-sq


1. a : Base
2. b : Base
3. c : a = b ∈ (⋂A:Type. (A ⟶ A ⟶ A))
4. a ~ λx,y. y
5. b ~ λx.if b x is lambda then λy.x otherwise ⊥
6. (λx,y. y) = (λx.if b x is lambda then λy.x otherwise ⊥) ∈ (ℕ ⟶ ℕ ⟶ ℕ)
⊢ (if a 0 1=0 then tt else ff ∈ (a ~ λx.if a x is lambda then λy.x otherwise ⊥) ∨ (a ~ a))
= (if b 0 1=0 then tt else ff ∈ (b ~ b) ∨ (b ~ a))
∈ Type
BY
{ ((Assert ⌜((λx,y. y) 0 1) = ((λx.if b x is lambda then λy.x otherwise ⊥) 0 1) ∈ ℕ⌝⋅
    THENA (ApFunToHypEquands `Z' ⌜Z 0 1⌝ ⌜ℕ⌝ (-1)⋅ THEN Auto)
    )
   THEN Reduce(-1)
   THEN (Assert ⌜if b 0 is lambda then λy.0 otherwise ⊥ 1 ~ 1⌝⋅ THENA Auto)
   THEN (Assert ⌜(if b 0 is lambda then λy.0 otherwise ⊥ 1)↓⌝⋅ THENA (RWO "-1" 0 THEN Auto))) }

1
1. a : Base
2. b : Base
3. c : a = b ∈ (⋂A:Type. (A ⟶ A ⟶ A))
4. a ~ λx,y. y
5. b ~ λx.if b x is lambda then λy.x otherwise ⊥
6. (λx,y. y) = (λx.if b x is lambda then λy.x otherwise ⊥) ∈ (ℕ ⟶ ℕ ⟶ ℕ)
7. 1 = (if b 0 is lambda then λy.0 otherwise ⊥ 1) ∈ ℕ
8. if b 0 is lambda then λy.0 otherwise ⊥ 1 ~ 1
9. (if b 0 is lambda then λy.0 otherwise ⊥ 1)↓
⊢ (if a 0 1=0 then tt else ff ∈ (a ~ λx.if a x is lambda then λy.x otherwise ⊥) ∨ (a ~ a))
= (if b 0 1=0 then tt else ff ∈ (b ~ b) ∨ (b ~ a))
∈ Type

---

Latex:

---

Latex:

1.  a  :  Base
2.  b  :  Base
3.  c  :  a  =  b
4.  a  \msim{}  \mlambda{}x,y.  y
5.  b  \msim{}  \mlambda{}x.if  b  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{}
6.  (\mlambda{}x,y.  y)  =  (\mlambda{}x.if  b  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})
\mvdash{}  (if  a  0  1=0  then  tt  else  ff  \mmember{}  (a  \msim{}  \mlambda{}x.if  a  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})  \mvee{}  (a  \msim{}  a))
=  (if  b  0  1=0  then  tt  else  ff  \mmember{}  (b  \msim{}  b)  \mvee{}  (b  \msim{}  a))


By

---

Latex:
((Assert  \mkleeneopen{}((\mlambda{}x,y.  y)  0  1)  =  ((\mlambda{}x.if  b  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})  0  1)\mkleeneclose{}\mcdot{}
    THENA  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  0  1\mkleeneclose{}  \mkleeneopen{}\mBbbN{}\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto)
    )
  THEN  Reduce(-1)
  THEN  (Assert  \mkleeneopen{}if  b  0  is  lambda  then  \mlambda{}y.0  otherwise  \mbot{}  1  \msim{}  1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(if  b  0  is  lambda  then  \mlambda{}y.0  otherwise  \mbot{}  1)\mdownarrow{}\mkleeneclose{}\mcdot{}  THENA  (RWO  "-1"  0  THEN  Auto)))

---

Home Index