---

Step * of Lemma bfs-reduce-strong-subtype-iff

∀[K:RngSig]. ∀[S,T:Type].
  ∀[as,bs:basic-formal-sum(K;S)].  (bfs-reduce(K;T;as;bs) ⇐⇒ bfs-reduce(K;S;as;bs)) supposing strong-subtype(S;T)
BY
{ (EAuto 1 THEN InstLemma `bfs-reduce-strong-subtype` [⌜K⌝;⌜S⌝;⌜T⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K:RngSig].  \mforall{}[S,T:Type].
    \mforall{}[as,bs:basic-formal-sum(K;S)].    (bfs-reduce(K;T;as;bs)  \mLeftarrow{}{}\mRightarrow{}  bfs-reduce(K;S;as;bs)) 
    supposing  strong-subtype(S;T)


By

---

Latex:
(EAuto  1  THEN  InstLemma  `bfs-reduce-strong-subtype`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index