---

Step * 1 2 2 of Lemma comp_id_mon_wf


1. T : Type
2. x : T ⟶ T
⊢ (Id o x) = x ∈ (T ⟶ T)
BY
{ BackThruLemma `comp_id_l` THEN Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T  {}\mrightarrow{}  T
\mvdash{}  (Id  o  x)  =  x


By

---

Latex:
BackThruLemma  `comp\_id\_l`  THEN  Auto

---

Home Index