---

Step * 1 1 1 1 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.if a x is lambda then λy.x otherwise ⊥
⊢ if if a 0 is lambda then λy.0 otherwise ⊥ 1=0 then tt else ff ∈ (a ~ a) ∨ (a ~ λx,y. y)
BY
{ ((Assert ⌜a ∈ ℕ ⟶ ℕ ⟶ ℕ⌝⋅ THENA Auto) THEN (Assert ⌜a 0 ∈ ℕ ⟶ ℕ⌝⋅ THENA Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mkleeneopen{}a  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (Assert  \mkleeneopen{}a  0  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index