Step
*
of Lemma
isvarterm_wf
No Annotations
∀[opr:Type]. ∀[t:term(opr)]. (isvarterm(t) ∈ 𝔹)
BY
{ ((InstLemma `term-ext` [] THEN ParallelLast)
THEN Intro
THEN Unhide
THEN (GenConcl ⌜t = x ∈ coterm-fun(opr;term(opr))⌝⋅ THENA Auto)
THEN (D -2 THEN RepUR ``isvarterm`` 0)
THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[opr:Type]. \mforall{}[t:term(opr)]. (isvarterm(t) \mmember{} \mBbbB{})
By
Latex:
((InstLemma `term-ext` [] THEN ParallelLast)
THEN Intro
THEN Unhide
THEN (GenConcl \mkleeneopen{}t = x\mkleeneclose{}\mcdot{} THENA Auto)
THEN (D -2 THEN RepUR ``isvarterm`` 0)
THEN Auto)
Home
Index