---

Step * 1 1 2 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 ⊥
5. b ~ λx.if b 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))
= (if if b 0 is lambda then λy.0 otherwise ⊥ 1=0 then tt else ff ∈ (b ~ b) ∨ (b ~ λx,y. y))
∈ Type
BY
{ ((Assert ⌜(λx.if a x is lambda then λy.x otherwise ⊥) = (λx.if b x is lambda then λy.x otherwise ⊥) ∈ (ℕ ⟶ ℕ ⟶ ℕ)⌝⋅
    THENA (RWO "-1<" 0 THEN RWO "-2<" 0 THEN Auto)
    )
   THEN (Assert ⌜((λx.if a x is lambda then λy.x otherwise ⊥) 0 1)
                 = ((λx.if b x is lambda then λy.x otherwise ⊥) 0 1)
                 ∈ ℕ⌝⋅
         THENA ((Assert ⌜λx.if a x is lambda then λy.x otherwise ⊥ ∈ ℕ ⟶ ℕ ⟶ ℕ⌝⋅ THENA Auto)
                THEN (Assert ⌜λx.if b x is lambda then λy.x otherwise ⊥ ∈ ℕ ⟶ ℕ ⟶ ℕ⌝⋅ THENA Auto)
                THEN GenConclAtAddr [2;1;1]
                THEN GenConclAtAddr [3;1;1]
                THEN Auto)
         )
   THEN Reduce(-1)) }

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

---

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


By

---

Latex:
((Assert  \mkleeneopen{}(\mlambda{}x.if  a  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})  =  (\mlambda{}x.if  b  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})\mkleeneclose{}
    \mcdot{}
    THENA  (RWO  "-1<"  0  THEN  RWO  "-2<"  0  THEN  Auto)
    )
  THEN  (Assert  \mkleeneopen{}((\mlambda{}x.if  a  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})  0  1)
                              =  ((\mlambda{}x.if  b  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{})  0  1)\mkleeneclose{}\mcdot{}
              THENA  ((Assert  \mkleeneopen{}\mlambda{}x.if  a  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{}  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  (Assert  \mkleeneopen{}\mlambda{}x.if  b  x  is  lambda  then  \mlambda{}y.x  otherwise  \mbot{}  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  GenConclAtAddr  [2;1;1]
                            THEN  GenConclAtAddr  [3;1;1]
                            THEN  Auto)
              )
  THEN  Reduce(-1))

---

Home Index