---

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


1. a : Base
2. b : Base
3. c : a = b ∈ (⋂A:Type. (A ⟶ A ⟶ A))
⊢ (if a 0 1=0 then tt else ff ∈ (a ~ λx.if a x is lambda then λy.x otherwise ⊥) ∨ (a ~ λx,y. y))
= (if b 0 1=0 then tt else ff ∈ (b ~ λx.if b x is lambda then λy.x otherwise ⊥) ∨ (b ~ λx,y. y))
∈ Type
BY
{ ((InstLemma `polymorphic-choice-base-sq` [⌜a⌝]⋅ THENA Auto)
   THEN (InstLemma `polymorphic-choice-base-sq` [⌜b⌝]⋅ THENA Auto)
   THEN DProdsAndUnions) }

1
1. a : Base
2. b : Base
3. c : a = b ∈ (⋂A:Type. (A ⟶ A ⟶ A))
4. a ~ λx.if a x is lambda then λy.x otherwise ⊥
5. b ~ λ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 ~ λx,y. y))
= (if b 0 1=0 then tt else ff ∈ (b ~ λx.if b x is lambda then λy.x otherwise ⊥) ∨ (b ~ λx,y. y))
∈ Type

2
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 ⊥
⊢ (if a 0 1=0 then tt else ff ∈ (a ~ λx.if a x is lambda then λy.x otherwise ⊥) ∨ (a ~ λx,y. y))
= (if b 0 1=0 then tt else ff ∈ (b ~ λx.if b x is lambda then λy.x otherwise ⊥) ∨ (b ~ λx,y. y))
∈ Type

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

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

---

Latex:

---

Latex:

1.  a  :  Base
2.  b  :  Base
3.  c  :  a  =  b
\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{}  \mlambda{}x,y.  y))
=  (if  b  0  1=0  then  tt  else  ff  \mmember{}  (b  \msim{}  \mlambda{}x.if  b  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})  \mvee{}  (b  \msim{}  \mlambda{}x,y.  y))


By

---

Latex:
((InstLemma  `polymorphic-choice-base-sq`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `polymorphic-choice-base-sq`  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DProdsAndUnions)

---

Home Index