---

Step * 1 2 1 of Lemma comp_id_mon_wf


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index