---

Step * of Lemma t-sqle-apply

∀[A,B:Type].  ∀a1,a2:A. ∀f1,f2:a:A ⟶ B.  (t-sqle(a:A ⟶ B;f1;f2) ⇒ t-sqle(A;a1;a2) ⇒ t-sqle(B;f1 a1;f2 a2))
BY
{ (Auto
   THEN All(Unfold `t-sqle`)
   THEN ExRepD
   THEN SquashExRepD
   THEN All(Unfold `per-class`)
   THEN DVarSets
   THEN D 0
   THEN InstConcl [⌜a3 a'⌝;⌜b1 b'⌝]⋅
   THEN Try (Complete (Auto))
   THEN Try ((MemTypeCD THEN Try (Complete (Auto))))
   THEN Try (Complete ((BLemma `equal-wf-base-T` THEN Auto)))
   THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))
   THEN BLemma `equal-wf-base-T`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}a1,a2:A.  \mforall{}f1,f2:a:A  {}\mrightarrow{}  B.    (t-sqle(a:A  {}\mrightarrow{}  B;f1;f2)  {}\mRightarrow{}  t-sqle(A;a1;a2)  {}\mRightarrow{}  t-sqle(B;f1  a1;f2  a2))


By

---

Latex:
(Auto
  THEN  All(Unfold  `t-sqle`)
  THEN  ExRepD
  THEN  SquashExRepD
  THEN  All(Unfold  `per-class`)
  THEN  DVarSets
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}a3  a'\mkleeneclose{};\mkleeneopen{}b1  b'\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((MemTypeCD  THEN  Try  (Complete  (Auto))))
  THEN  Try  (Complete  ((BLemma  `equal-wf-base-T`  THEN  Auto)))
  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  BLemma  `equal-wf-base-T`
  THEN  Auto)

---

Home Index