---

Step * of Lemma istype-inl-sqeq-inr

∀[a,b:Top].  istype(inl a ~ inr b )
BY
{ (TACTIC:Intros
   THEN At ⌜Type⌝ (D 0)⋅
   THEN PointwiseFunctionality 1
   THEN PointwiseFunctionality (-1)
   THEN Repeat (((EqCDA ORELSE Unfold `member` 0) THEN Try (Refine_sqequalExtensionalEquality)))
   THEN RepeatFor 3 ((D 0 THENW Auto))
   THEN InstLemma `not-inl-sqeq-inr` []
   THEN Auto
   THEN (Unfold `not` -1 THEN FHyp (-1) [-2])
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:Top].    istype(inl  a  \msim{}  inr  b  )


By

---

Latex:
(TACTIC:Intros
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}
  THEN  PointwiseFunctionality  1
  THEN  PointwiseFunctionality  (-1)
  THEN  Repeat  (((EqCDA  ORELSE  Unfold  `member`  0)  THEN  Try  (Refine\_sqequalExtensionalEquality)))
  THEN  RepeatFor  3  ((D  0  THENW  Auto))
  THEN  InstLemma  `not-inl-sqeq-inr`  []
  THEN  Auto
  THEN  (Unfold  `not`  -1  THEN  FHyp  (-1)  [-2])
  THEN  Auto)

---

Home Index