---

Step * 1 1 of Lemma op-op-cat

.....subterm..... T:t
2:n
1. ob : Type
2. arrow : ob ⟶ ob ⟶ Type
3. C3 : x:ob ⟶ (arrow x x)
4. C4 : x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z)
⊢ C4 = (λx,y,z,f,g. (C4 x y z f g)) ∈ (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))
BY
{ TACTIC:RepeatFor 3 ((Ext THEN Reduce 0 THEN Auto)) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  ob  :  Type
2.  arrow  :  ob  {}\mrightarrow{}  ob  {}\mrightarrow{}  Type
3.  C3  :  x:ob  {}\mrightarrow{}  (arrow  x  x)
4.  C4  :  x:ob  {}\mrightarrow{}  y:ob  {}\mrightarrow{}  z:ob  {}\mrightarrow{}  (arrow  x  y)  {}\mrightarrow{}  (arrow  y  z)  {}\mrightarrow{}  (arrow  x  z)
\mvdash{}  C4  =  (\mlambda{}x,y,z,f,g.  (C4  x  y  z  f  g))


By

---

Latex:
TACTIC:RepeatFor  3  ((Ext  THEN  Reduce  0  THEN  Auto))

---

Home Index