---

Step * of Lemma partial-partial

∀[A:Type]. (partial(partial(A)) ⊆r partial(A))
BY
{ TACTIC:(Auto THEN (D 0 THENA Auto) THEN (D -1 THENA Auto) THEN EqTypeCD THEN Auto) }

1
.....antecedent..... 
1. A : Type
2. x : Base
3. x1 : Base
4. x
= x1
∈ pertype(λx,y. ((x ∈ base-partial(partial(A))) ∧ (y ∈ base-partial(partial(A))) ∧ per-partial(partial(A);x;y)))
5. x ∈ base-partial(partial(A))
6. x1 ∈ base-partial(partial(A))
7. per-partial(partial(A);x;x1)
⊢ per-partial(A;x;x1)

---

Latex:

---

Latex:
\mforall{}[A:Type].  (partial(partial(A))  \msubseteq{}r  partial(A))


By

---

Latex:
TACTIC:(Auto  THEN  (D  0  THENA  Auto)  THEN  (D  -1  THENA  Auto)  THEN  EqTypeCD  THEN  Auto)

---

Home Index