---

Step * 1 2 of Lemma ctt-opr-is-implies

.....falsecase..... 
1. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
2. f1 : if k =a "nType" then Type
if k =a "nterm" then T:Type × T
else ℕ
fi 
3. s : Atom
4. ↑(k =a "opid" ∧b f1 =a s)
5. ¬(k = "opid" ∈ Atom)
⊢ <k, f1> = <"opid", s> ∈ (Atom × Atom)
BY
{ (Subst' k =a "opid" ~ ff -2 THENA Auto) }

1
1. k : {k:Atom| (k ∈ ``opid nType nterm univ``)} 
2. f1 : if k =a "nType" then Type
if k =a "nterm" then T:Type × T
else ℕ
fi 
3. s : Atom
4. ↑(ff ∧b f1 =a s)
5. ¬(k = "opid" ∈ Atom)
⊢ <k, f1> = <"opid", s> ∈ (Atom × Atom)

---

Latex:

---

Latex:
.....falsecase..... 
1.  k  :  \{k:Atom|  (k  \mmember{}  ``opid  nType  nterm  univ``)\} 
2.  f1  :  if  k  =a  "nType"  then  Type
if  k  =a  "nterm"  then  T:Type  \mtimes{}  T
else  \mBbbN{}
fi 
3.  s  :  Atom
4.  \muparrow{}(k  =a  "opid"  \mwedge{}\msubb{}  f1  =a  s)
5.  \mneg{}(k  =  "opid")
\mvdash{}  <k,  f1>  =  <"opid",  s>


By

---

Latex:
(Subst'  k  =a  "opid"  \msim{}  ff  -2  THENA  Auto)

---

Home Index