---

Step * of Lemma tag-by-subtype-tag-case

∀[T,S:Type].  ∀z,x:Atom.  (z×T ⊆r x:S ⇐⇒ (¬↑z =a x) ∨ (T ⊆r S))
BY
{ ((UnivCD THENA Auto)
   THEN AutoBoolCase ⌜z =a x⌝
   ⋅
   THEN Auto
   THEN SplitOrHyps
   THEN Auto
   THEN Try ((Sel 1 (D 0) THEN Complete (Auto)))
   THEN Try ((Sel 2 (D 0) THEN Auto))
   THEN Try ((D 0 THEN Auto))
   THEN Try ((All (Unfolds ``tag-case tag-by``)
              THEN D -1
              THEN Try (D -2)
              THEN Auto
              THEN SplitOnConclITE
              THEN Auto
              THEN OnMaybeHyp 5 (\h. (D h THEN Eq)))⋅)) }

1
.....subterm..... T:t
1:n
1. T : Type
2. S : Type
3. z : Atom
4. x : Atom
5. z = x ∈ Atom
6. z×T ⊆r x:S
7. x1 : T
⊢ x1 ∈ S

---

Latex:

---

Latex:
\mforall{}[T,S:Type].    \mforall{}z,x:Atom.    (z\mtimes{}T  \msubseteq{}r  x:S  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}\muparrow{}z  =a  x)  \mvee{}  (T  \msubseteq{}r  S))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}z  =a  x\mkleeneclose{}
  \mcdot{}
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  ((Sel  1  (D  0)  THEN  Complete  (Auto)))
  THEN  Try  ((Sel  2  (D  0)  THEN  Auto))
  THEN  Try  ((D  0  THEN  Auto))
  THEN  Try  ((All  (Unfolds  ``tag-case  tag-by``)
                        THEN  D  -1
                        THEN  Try  (D  -2)
                        THEN  Auto
                        THEN  SplitOnConclITE
                        THEN  Auto
                        THEN  OnMaybeHyp  5  (\mbackslash{}h.  (D  h  THEN  Eq)))\mcdot{}))

---

Home Index