---

Step * of Lemma subtype_rel_quotient

∀[A,B:Type]. ∀[E:B ⟶ B ⟶ ℙ].  ((x,y:A//E[x;y]) ⊆r (x,y:B//E[x;y])) supposing (EquivRel(B;x,y.E[x;y]) and (A ⊆r B))
BY
{ (Auto THEN D 0 THEN Auto THEN Try ((FLemma `equiv_rel_subtype` [-2;-1] THEN Auto))) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. E : B ⟶ B ⟶ ℙ
4. A ⊆r B
5. EquivRel(B;x,y.E[x;y])
6. x : x,y:A//E[x;y]@i
⊢ x ∈ x,y:B//E[x;y]

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[E:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].
    ((x,y:A//E[x;y])  \msubseteq{}r  (x,y:B//E[x;y]))  supposing  (EquivRel(B;x,y.E[x;y])  and  (A  \msubseteq{}r  B))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  Try  ((FLemma  `equiv\_rel\_subtype`  [-2;-1]  THEN  Auto)))

---

Home Index