Step
*
of Lemma
alpha-eq-terms_weakening
No Annotations
∀[opr:Type]. ∀a,b:term(opr).  ((a = b ∈ term(opr)) 
⇒ alpha-eq-terms(opr;b;a))
BY
{ ((InstLemma `alpha-eq-equiv-rel` [] THEN ParallelLast) THEN D -1 THEN Auto) }
Latex:
Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}a,b:term(opr).    ((a  =  b)  {}\mRightarrow{}  alpha-eq-terms(opr;b;a))
By
Latex:
((InstLemma  `alpha-eq-equiv-rel`  []  THEN  ParallelLast)  THEN  D  -1  THEN  Auto)
Home
Index