---

Step * of Lemma t-sqle_reflexive

∀[T:Type]. ∀a:T. t-sqle(T;a;a)
BY
{ (Auto THEN (InstLemma `squash-per-class` [⌜T⌝;⌜a⌝]⋅ THENA Auto)) }

1
1. T : Type
2. a : T@i
3. ↓per-class(T;a)
⊢ t-sqle(T;a;a)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}a:T.  t-sqle(T;a;a)


By

---

Latex:
(Auto  THEN  (InstLemma  `squash-per-class`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index