---

Step * 1 2 of Lemma comp_id_mon_wf


1. T : Type
⊢ Ident(T ⟶ T;λf,g. (f o g);Id)
BY
{ Unfold `ident` 0 
THEN AbReduce 0 
THEN GenUnivCD THENA Auto }

1
1. T : Type
2. x : T ⟶ T
⊢ (x o Id) = x ∈ (T ⟶ T)

2
1. T : Type
2. x : T ⟶ T
⊢ (Id o x) = x ∈ (T ⟶ T)

---

Latex:

---

Latex:

1.  T  :  Type
\mvdash{}  Ident(T  {}\mrightarrow{}  T;\mlambda{}f,g.  (f  o  g);Id)


By

---

Latex:
Unfold  `ident`  0 
THEN  AbReduce  0 
THEN  GenUnivCD  THENA  Auto

---

Home Index